## cool / src / lib / CoAlgMisc.ml @ 7c4d2eb4

History | View | Annotate | Download (26.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 | type t = S.bitset |
||

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

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

28 | end |
||

29 | ) |
||

30 | |||

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

32 | *) |
||

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

34 | struct |
||

35 | type t = Minisat.lit |
||

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

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

38 | end |
||

39 | ) |
||

40 | |||

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

42 | *) |
||

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

44 | struct |
||

45 | type t = int |
||

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

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

48 | end |
||

49 | ) |
||

50 | |||

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

52 | *) |
||

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

54 | struct |
||

55 | type t = int * int |
||

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

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

58 | end |
||

59 | ) |
||

60 | |||

61 | |||

62 | (*****************************************************************************) |
||

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

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

65 | (*****************************************************************************) |
||

66 | |||

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

68 | type functors = |
||

69 | | MultiModalK |
||

70 | a87192e8 | Thorsten Wißmann | | MultiModalKD |

71 | f1fa9ad5 | Thorsten Wißmann | | CoalitionLogic |

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

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

74 | | Fusion |
||

75 | |||

76 | (* This type may be extended for additional logics. *) |
||

77 | type formulaType = |
||

78 | | Other |
||

79 | | ConstF |
||

80 | | AndF |
||

81 | | OrF |
||

82 | | AtF |
||

83 | | NomF |
||

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

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

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

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

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

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

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

91 | | FusF (* Fusion *) |
||

92 | 4fd28192 | Thorsten Wißmann | |

93 | type localFormula = int |
||

94 | type bset = S.bitset |
||

95 | |||

96 | type atFormula = int |
||

97 | type cset = S.bitset |
||

98 | type csetSet = BsSet.t |
||

99 | |||

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

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

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

103 | |||

104 | type state = { sortS : sort; mutable bsS : bset; mutable statusS : nodeStatus; |
||

105 | mutable parentsS : core list; mutable childrenS : (dependencies * core list) list; |
||

106 | mutable constraintsS : csetSet; expandFkt : stateExpander } |
||

107 | |||

108 | and core = { sortC : sort; mutable bsC : bset; mutable statusC : nodeStatus; |
||

109 | mutable parentsC : (state * int) list; mutable childrenC : state list; |
||

110 | mutable constraintsC : csetSet; solver : Minisat.solver; fht : fht; |
||

111 | mutable constraintParents : cset list } |
||

112 | |||

113 | and setState = state GHt.t |
||

114 | |||

115 | and setCore = core GHt.t |
||

116 | |||

117 | and setCnstr = unit GHt.t |
||

118 | |||

119 | |||

120 | (*****************************************************************************) |
||

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

122 | (*****************************************************************************) |
||

123 | |||

124 | and stateExpander = unit -> ruleEnumeration |
||

125 | |||

126 | and sort = C.sort |
||

127 | |||

128 | and nodeStatus = |
||

129 | | Expandable |
||

130 | | Open |
||

131 | | Sat |
||

132 | | Unsat |
||

133 | |||

134 | and dependencies = bset list -> bset |
||

135 | and ruleEnumeration = |
||

136 | | AllInOne of (dependencies * (sort * bset) list) list |
||

137 | | NextRule of dependencies * (sort * bset) list |
||

138 | | NoMoreRules |
||

139 | |||

140 | type nominal = sort * localFormula |
||

141 | |||

142 | type node = |
||

143 | | State of state |
||

144 | | Core of core |
||

145 | |||

146 | type constrnt = |
||

147 | | UnsatC |
||

148 | | SatC |
||

149 | | OpenC of node list |
||

150 | | UnexpandedC of node list |
||

151 | |||

152 | type propagateElement = |
||

153 | | UState of state * int option |
||

154 | | UCore of core * bool |
||

155 | | UCnstr of cset |
||

156 | |||

157 | type queueElement = |
||

158 | | QState of state |
||

159 | | QCore of core |
||

160 | | QCnstr of cset |
||

161 | | QEmpty |
||

162 | |||

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

164 | |||

165 | exception CoAlg_finished of bool |
||

166 | |||

167 | |||

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

169 | |||

170 | |||

171 | (*****************************************************************************) |
||

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

173 | (*****************************************************************************) |
||

174 | |||

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

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

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

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

179 | let doPropagation = ref false |
||

180 | |||

181 | let queueInit () = |
||

182 | queueStates := []; |
||

183 | queueCores1 := []; |
||

184 | queueCores2 := []; |
||

185 | queueCnstrs := []; |
||

186 | doPropagation := false |
||

187 | |||

188 | let queueIsEmpty () = |
||

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

190 | |||

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

192 | |||

193 | let queueInsertCore core = queueCores2 := core::!queueCores2 |
||

194 | |||

195 | let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs |
||

196 | |||

197 | let queueGetElement () = |
||

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

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

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

201 | QCnstr res |
||

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

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

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

205 | QState res |
||

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

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

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

209 | QCore res |
||

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

211 | else |
||

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

213 | doPropagation := true; |
||

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

215 | queueCores2 := []; |
||

216 | QCore res |
||

217 | |||

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

219 | |||

220 | let doSatPropagation () = |
||

221 | let res = !doPropagation in |
||

222 | doPropagation := false; |
||

223 | res |
||

224 | |||

225 | |||

226 | (*****************************************************************************) |
||

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

228 | (*****************************************************************************) |
||

229 | |||

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

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

232 | let graphCnstrs = ref (GHt.create 0 : constrnt GHt.t) |
||

233 | let graphRoot = ref (None : core option) |
||

234 | |||

235 | let graphInit () = |
||

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

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

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

239 | graphCnstrs := GHt.create 128; |
||

240 | graphRoot := None |
||

241 | |||

242 | let graphIterStates fkt = |
||

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

244 | |||

245 | let graphIterCores fkt = |
||

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

247 | |||

248 | let graphIterCnstrs fkt = GHt.iter fkt !graphCnstrs |
||

249 | |||

250 | let graphClearCnstr () = |
||

251 | let newGraph = GHt.create (GHt.length !graphCnstrs) in |
||

252 | let copyCnstr cset cnstr = |
||

253 | match cnstr with |
||

254 | | UnsatC |
||

255 | | SatC -> GHt.add newGraph cset cnstr |
||

256 | | OpenC _ -> GHt.add newGraph cset (OpenC []) |
||

257 | | UnexpandedC _ -> GHt.add newGraph cset (UnexpandedC []) |
||

258 | in |
||

259 | GHt.iter copyCnstr !graphCnstrs; |
||

260 | graphCnstrs := newGraph |
||

261 | |||

262 | let graphFindState sort bs = |
||

263 | try |
||

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

265 | with Not_found -> None |
||

266 | |||

267 | let graphFindCore sort bs = |
||

268 | try |
||

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

270 | with Not_found -> None |
||

271 | |||

272 | let graphFindCnstr cset = |
||

273 | try |
||

274 | Some (GHt.find !graphCnstrs cset) |
||

275 | with Not_found -> None |
||

276 | |||

277 | let graphInsertState sort bs state = |
||

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

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

280 | |||

281 | let graphInsertCore sort bs core = |
||

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

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

284 | |||

285 | let graphInsertCnstr cset cnstr = |
||

286 | assert (not (GHt.mem !graphCnstrs cset)); |
||

287 | GHt.add !graphCnstrs cset cnstr |
||

288 | |||

289 | let graphReplaceCnstr cset cnstr = |
||

290 | GHt.replace !graphCnstrs cset cnstr |
||

291 | |||

292 | let graphSizeState () = |
||

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

294 | let graphSizeCore () = |
||

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

296 | let graphSizeCnstr () = GHt.length !graphCnstrs |
||

297 | |||

298 | let graphAddRoot core = |
||

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

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

301 | |||

302 | let graphGetRoot () = |
||

303 | match !graphRoot with |
||

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

305 | | Some core -> core |
||

306 | |||

307 | |||

308 | (*****************************************************************************) |
||

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

310 | (*****************************************************************************) |
||

311 | |||

312 | let cssEmpty = BsSet.empty |
||

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

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

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

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

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

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

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

320 | |||

321 | |||

322 | (*****************************************************************************) |
||

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

324 | (*****************************************************************************) |
||

325 | |||

326 | let stateMake sort bs exp = |
||

327 | { sortS = sort; bsS = bs; statusS = Expandable; parentsS = []; childrenS = []; |
||

328 | constraintsS = cssEmpty; expandFkt = exp } |
||

329 | let stateGetSort state = state.sortS |
||

330 | let stateGetBs state = state.bsS |
||

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

332 | let stateGetStatus state = state.statusS |
||

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

334 | let stateGetParents state = state.parentsS |
||

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

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

337 | let stateGetRules state = state.childrenS |
||

338 | let stateAddRule state dep children = |
||

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

340 | List.length state.childrenS |
||

341 | let stateGetConstraints state = state.constraintsS |
||

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

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

344 | |||

345 | |||

346 | (*****************************************************************************) |
||

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

348 | (*****************************************************************************) |
||

349 | |||

350 | let coreMake sort bs solver fht = |
||

351 | { sortC = sort; bsC = bs; statusC = Expandable; parentsC = []; childrenC = []; |
||

352 | constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [] } |
||

353 | let coreGetSort core = core.sortC |
||

354 | let coreGetBs core = core.bsC |
||

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

356 | let coreGetStatus core = core.statusC |
||

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

358 | let coreGetParents core = core.parentsC |
||

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

360 | let coreGetChildren core = core.childrenC |
||

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

362 | let coreGetConstraints core = core.constraintsC |
||

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

364 | let coreGetSolver core = core.solver |
||

365 | let coreGetFht core = core.fht |
||

366 | let coreGetConstraintParents core = core.constraintParents |
||

367 | let coreAddConstraintParent core cset = |
||

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

369 | |||

370 | |||

371 | (*****************************************************************************) |
||

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

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

374 | (*****************************************************************************) |
||

375 | |||

376 | let setEmptyState () = GHt.create 16 |
||

377 | let setEmptyCore () = GHt.create 16 |
||

378 | let setEmptyCnstr () = GHt.create 16 |
||

379 | let setAddState set state = GHt.add set (stateGetBs state) state |
||

380 | let setAddCore set core = GHt.add set (coreGetBs core) core |
||

381 | let setAddCnstr set cset = GHt.add set cset () |
||

382 | let setMemState set state = GHt.mem set (stateGetBs state) |
||

383 | let setMemCore set core = GHt.mem set (coreGetBs core) |
||

384 | let setMemCnstr set cset = GHt.mem set cset |
||

385 | let setRemoveState set state = GHt.remove set (stateGetBs state) |
||

386 | let setRemoveCore set core = GHt.remove set (coreGetBs core) |
||

387 | let setRemoveCnstr set cset = GHt.remove set cset |
||

388 | let setIterState fkt set = GHt.iter (fun _ state -> fkt state) set |
||

389 | let setIterCore fkt set = GHt.iter (fun _ core -> fkt core) set |
||

390 | let setIterCnstr fkt set = GHt.iter (fun cset () -> fkt cset) set |
||

391 | |||

392 | |||

393 | (*****************************************************************************) |
||

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

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

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

397 | (*****************************************************************************) |
||

398 | |||

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

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

401 | let lhtFind lht lit = |
||

402 | try |
||

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

404 | with Not_found -> None |
||

405 | |||

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

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

408 | let fhtFind fht f = |
||

409 | try |
||

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

411 | with Not_found -> None |
||

412 | |||

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

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

415 | let nhtFind nht nom = |
||

416 | try |
||

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

418 | with Not_found -> None |
||

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

420 | |||

421 | (*****************************************************************************) |
||

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

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

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

425 | |||

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

427 | |||

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

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

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

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

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

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

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

435 | res |
||

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

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

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

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

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

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

442 | res |
||

443 | |||

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

445 | |||

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

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

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

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

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

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

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

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

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

455 | let csetIter cs fkt = |
||

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

457 | S.iterBS fkt2 cs |
||

458 | |||

459 | |||

460 | (*****************************************************************************) |
||

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

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

463 | (*****************************************************************************) |
||

464 | |||

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

466 | *) |
||

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

468 | |||

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

470 | *) |
||

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

472 | |||

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

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

475 | *) |
||

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

477 | |||

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

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

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

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

482 | *) |
||

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

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

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

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

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

488 | 4fd28192 | Thorsten Wißmann | |

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

490 | to their @-wrapper. |
||

491 | *) |
||

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

493 | |||

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

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

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

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

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

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

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

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

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

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

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

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

506 | let lfFromInt num = num |
||

507 | 4fd28192 | Thorsten Wißmann | |

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

509 | let atFormulaGetNominal f = |
||

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

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

512 | (s, n) |
||

513 | |||

514 | let lfToAt _ lf = lf |
||

515 | |||

516 | |||

517 | let rec detClosure nomTbl hcF fset atset nomset s f = |
||

518 | if s < 0 || s >= Array.length fset then |
||

519 | let sstr = string_of_int s in |
||

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

521 | else (); |
||

522 | if C.HcFHt.mem fset.(s) f then () |
||

523 | else |
||

524 | let () = C.HcFHt.add fset.(s) f () in |
||

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

526 | match f.HC.node with |
||

527 | | C.HCTRUE |
||

528 | | C.HCFALSE -> () |
||

529 | | C.HCAP name -> |
||

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

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

532 | match nomTbl name with |
||

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

534 | | Some sort -> |
||

535 | if sort <> s then |
||

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

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

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

539 | else () |
||

540 | end else () |
||

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

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

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

544 | let s1 = |
||

545 | match nomTbl name with |
||

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

547 | | Some sort -> sort |
||

548 | in |
||

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

550 | detClosure nomTbl hcF fset atset nomset s1 hcnom; |
||

551 | detClosure nomTbl hcF fset atset nomset s1 f1 |
||

552 | | C.HCOR (f1, f2) |
||

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

554 | detClosure nomTbl hcF fset atset nomset s f1; |
||

555 | detClosure nomTbl hcF fset atset nomset s f2 |
||

556 | | C.HCEX (_, f1) |
||

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

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

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

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

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

562 | detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 |
||

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

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

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

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

567 | else (); |
||

568 | detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 |
||

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

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

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

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

573 | else (); |
||

574 | detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1 |
||

575 | 4fd28192 | Thorsten Wißmann | | C.HCCHC (f1, f2) |

576 | | C.HCCHCN (f1, f2) -> |
||

577 | if func <> Choice || List.length sortlst <> 2 then |
||

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

579 | else (); |
||

580 | detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1; |
||

581 | detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2 |
||

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

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

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

585 | else (); |
||

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

587 | detClosure nomTbl hcF fset atset nomset s1 f1 |
||

588 | |||

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

590 | match f.HC.node with |
||

591 | | C.HCTRUE |
||

592 | | C.HCFALSE |
||

593 | | C.HCOR _ |
||

594 | | C.HCAND _ |
||

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

596 | | _ -> |
||

597 | let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in |
||

598 | C.HcFHt.replace atset at () |
||

599 | |||

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

601 | *) |
||

602 | let initTables nomTbl hcF htF htR s f n = |
||

603 | !arrayFormula.(s).(n) <- f.HC.fml; |
||

604 | let fneg = f.HC.neg in |
||

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

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

607 | match f.HC.node with |
||

608 | | C.HCTRUE |
||

609 | | C.HCFALSE -> !arrayType.(s).(n) <- ConstF |
||

610 | | C.HCAP name -> |
||

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

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

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

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

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

616 | let s1 = |
||

617 | match nomTbl name with |
||

618 | | None -> assert false |
||

619 | | Some sort -> sort |
||

620 | in |
||

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

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

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

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

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

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

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

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

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

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

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

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

633 | | C.HCEX (role, f1) -> |
||

634 | !arrayType.(s).(n) <- ExF; |
||

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

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

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

638 | else |
||

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

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

641 | size |
||

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

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

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

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

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

647 | else |
||

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

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

650 | size |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

665 | else |
||

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

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

668 | size |
||

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

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

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

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

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

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

675 | else |
||

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

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

678 | size |
||

679 | 4fd28192 | Thorsten Wißmann | | C.HCCHC (f1, f2) |

680 | | C.HCCHCN (f1, f2) -> |
||

681 | !arrayType.(s).(n) <- ChcF; |
||

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

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

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

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

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

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

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

689 | |||

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

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

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

693 | let addAt f n = |
||

694 | match f.HC.node with |
||

695 | | C.HCTRUE |
||

696 | | C.HCFALSE |
||

697 | | C.HCOR _ |
||

698 | | C.HCAND _ |
||

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

700 | | _ -> |
||

701 | let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in |
||

702 | let atn = C.HcFHt.find htF.(0) at in |
||

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

704 | in |
||

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

706 | |||

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

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

709 | if card <= 0 then |
||

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

711 | else (); |
||

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

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

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

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

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

717 | |||

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

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

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

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

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

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

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

725 | 4fd28192 | Thorsten Wißmann | |

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

727 | let atset = C.HcFHt.create 64 in |
||

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

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

730 | detClosure nomTbl hcF fset atset nomset i hcfalse; |
||

731 | detClosure nomTbl hcF fset atset nomset i hctrue; |
||

732 | done; |
||

733 | f828ad2f | Thorsten Wißmann | detClosure nomTbl hcF fset atset nomset s hcf; |

734 | detClosure nomTbl hcF fset atset nomset s nhcf; |
||

735 | List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox; |
||

736 | List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox; |
||

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

738 | |||

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

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

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

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

743 | done; |
||

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

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

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

747 | done; |
||

748 | idx + 1 |
||

749 | in |
||

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

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

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

753 | else begin |
||

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

755 | idx+1 |
||

756 | end |
||

757 | in |
||

758 | let size = ref 0 in |
||

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

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

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

762 | done; |
||

763 | |||

764 | arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); |
||

765 | arrayType := Array.init card (fun _ -> Array.make !size Other); |
||

766 | arrayDest1 := Array.init card (fun _ -> Array.make !size (-1)); |
||

767 | arrayDest2 := Array.init card (fun _ -> Array.make !size (-1)); |
||

768 | arrayDest3 := Array.init card (fun _ -> Array.make !size (-1)); |
||

769 | arrayNeg := Array.init card (fun _ -> Array.make !size (-1)); |
||

770 | 29b2e3f3 | Thorsten Wißmann | arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); |

771 | 98af95fb | Thorsten Wißmann | arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); |

772 | 4fd28192 | Thorsten Wißmann | let htR = Hashtbl.create 128 in |

773 | Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF; |
||

774 | arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8)); |
||

775 | Hashtbl.iter (initTablesAt hcF htF) nomset; |
||

776 | |||

777 | S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1); |
||

778 | let initbs = bsetMake () in |
||

779 | bsetAdd initbs (C.HcFHt.find htF.(s) hcf); |
||

780 | let tboxTbl = Array.init card (fun _ -> bsetMake ()) in |
||

781 | List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox; |
||

782 | tboxTable := tboxTbl; |
||

783 | (tbox1, (s, f1), initbs) |