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

History | View | Annotate | Download (26.8 KB)

1 |
(** Common types, functions, and data structures for the CoAlgebraic reasoner. |
---|---|

2 |
@author Florian Widmann |

3 |
*) |

4 | |

5 | |

6 |
module S = MiscSolver |

7 |
module L = List |

8 |
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 |
| MultiModalKD |

71 |
| CoalitionLogic |

72 |
| GML |

73 |
| 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 |
| ExF (* Existential / diamond *) |

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

86 |
| EnforcesF (* diamond of CL *) |

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

88 |
| MoreThanF (* more than n successors = diamond in gml *) |

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

90 |
| ChcF (* Choice *) |

91 |
| FusF (* Fusion *) |

92 | |

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 |
let bsetRem bs lf = S.remBS bs lf |

432 |
let bsetMakeRealEmpty () = |

433 |
let res = bsetMake () in |

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

435 |
res |

436 |
let bsetCopy bs = S.copyBS bs |

437 |
let bsetFold fkt bs init = S.foldBS fkt bs init |

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

439 |
let bsetFilter (a: bset) (f: localFormula -> bool) : bset = |

440 |
let res = bsetMakeRealEmpty () in |

441 |
bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a; |

442 |
res |

443 | |

444 |
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 |
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 |
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *) |

487 |
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *) |

488 | |

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 |
let lfGetDestNum sort f = !arrayDestNum.(sort).(f) |

499 |
let lfGetDestAg sort f = !arrayDestAg.(sort).(f) |

500 |
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 |
let lfToInt lf = lf |

506 |
let lfFromInt num = num |

507 | |

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 |
if (func <> MultiModalK && func <> MultiModalKD) |

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

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

561 |
else (); |

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

563 |
| 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 |
| C.HCMORETHAN (_,_,f1) |

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

571 |
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 |
| 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 |
| 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 |
| C.HCMORETHAN (cnt,role,f1) -> |

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

661 |
!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 |
| C.HCMAXEXCEPT (cnt,role,f1) -> |

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

671 |
!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 |
| 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 |
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 |
let hcfalse = C.hc_formula hcF C.FALSE in |

724 |
let hctrue = C.hc_formula hcF C.TRUE in |

725 | |

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 |
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 |
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 |
arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); |

771 |
arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); |

772 |
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) |