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

History | View | Annotate | Download (45.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 * 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 |
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 |
| MultiModalKD |

82 |
| CoalitionLogic |

83 |
| GML |

84 |
| PML |

85 |
| Constant of string list |

86 |
| Identity |

87 |
| DefaultImplication |

88 |
| Choice |

89 |
| Fusion |

90 | |

91 |
(* functors whose constructor takes additional parameters *) |

92 |
type parametricFunctorName = |

93 |
| NameConstant |

94 | |

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

96 |
type functorName = |

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

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

99 | |

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

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

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

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

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

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

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

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

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

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

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

111 |
; (NPa Identity, "Id") |

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

113 |
] |

114 | |

115 |
let functor2name : (functorName*string) list = |

116 |
L.append unaryfunctor2name |

117 |
[ (NPa Choice , "Choice") |

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

119 |
] |

120 | |

121 |
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option = |

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

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

124 |
match func with |

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

126 | |

127 | |

128 |
let functor_of_string str params : functors option = |

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

130 |
try |

131 |
let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in |

132 |
match functorName with |

133 |
| NPa x -> Some x |

134 |
| Pa f -> functor_apply_parameters f params |

135 |
with Not_found -> None |

136 | |

137 |
let unaryfunctor_of_string str params = |

138 |
match (functor_of_string str params) with |

139 |
| Some Choice -> None |

140 |
| Some Fusion -> None |

141 |
| x -> x |

142 | |

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

144 |
(* replace f orrectly with possibly some Pa wrapper *) |

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

146 |
let f,suffix = match f with |

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

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

149 |
in |

150 |
let snd (a,b) = b in |

151 |
try |

152 |
let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in |

153 |
name ^ suffix |

154 |
with Not_found -> assert false |

155 | |

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

157 |
type formulaType = |

158 |
| Other |

159 |
| TrueFalseF (* constant true or false *) |

160 |
| AndF |

161 |
| OrF |

162 |
| AtF |

163 |
| NomF |

164 |
| ExF (* Existential / diamond *) |

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

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

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

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

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

170 |
| AtLeastProbF (* for PML *) |

171 |
| LessProbFailF (* box for PML *) |

172 |
| ConstF (* constant functor *) |

173 |
| ConstnF (* constant functor *) |

174 |
| IdF (* Identity functor *) |

175 |
| NormF (* Default Implication *) |

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

177 |
| ChcF (* Choice *) |

178 |
| FusF (* Fusion *) |

179 |
| MuF |

180 |
| NuF |

181 | |

182 |
type localFormula = int |

183 |
type bset = S.bitset |

184 | |

185 |
type atFormula = int |

186 |
type cset = S.bitset |

187 |
type csetSet = BsSet.t |

188 | |

189 |
type lht = localFormula LHt.t |

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

191 |
type nht = bset NHt.t |

192 | |

193 |
type state = { sortS : sort; |

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

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

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

197 |
*) |

198 |
mutable deferralS : bset; (* which formulas still have deferrals *) |

199 |
mutable statusS : nodeStatus; |

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

201 |
mutable constraintsS : csetSet; expandFkt : stateExpander; |

202 |
idx: int } |

203 | |

204 |
and core = { (* for details, see documentation of newCore *) |

205 |
sortC : sort; |

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

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

208 |
mutable deferralC : bset; (* which formulas still have deferrals *) |

209 |
mutable statusC : nodeStatus; |

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

211 |
mutable childrenC : state list; |

212 |
mutable constraintsC : csetSet; |

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

214 |
the solver returns "satisfiable" iff |

215 |
there is a satisfying assignment of |

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

217 |
childrenC yet. |

218 |
*) |

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

220 |
of the Minisat solver |

221 |
*) |

222 |
mutable constraintParents : cset list; |

223 |
idx : int } |

224 | |

225 |
and setState = state GHt.t array |

226 | |

227 |
and setCore = core GHt.t array |

228 | |

229 |
and setCnstr = unit GHtS.t |

230 | |

231 | |

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

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

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

235 | |

236 |
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *) |

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

238 | |

239 |
and stateExpander = rule lazylist |

240 | |

241 |
and sort = C.sort |

242 | |

243 |
and nodeStatus = |

244 |
| Expandable |

245 |
| Open |

246 |
| Sat |

247 |
| Unsat |

248 | |

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

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

251 |
as well as the Ex. |

252 | |

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

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

255 |
*) |

256 |
and dependencies = bset list -> bset |

257 | |

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

259 |
and rule = (dependencies * (sort * bset * bset) lazylist) |

260 | |

261 |
and 'a lazyliststep = |

262 |
| MultipleElements of 'a list |

263 |
| SingleElement of 'a |

264 |
| NoMoreElements |

265 | |

266 |
and 'a lazylist = unit -> 'a lazyliststep |

267 | |

268 |
and ruleEnumeration = rule lazyliststep |

269 | |

270 |
let nodeStatusToString : nodeStatus -> string = function |

271 |
| Expandable -> "Expandable" |

272 |
| Open -> "Open" |

273 |
| Sat -> "Sat" |

274 |
| Unsat -> "Unsat" |

275 | |

276 |
let lazylistFromList a_list = |

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

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

279 |
| Some (a_list) -> begin |

280 |
list_state := None; |

281 |
MultipleElements a_list |

282 |
end |

283 |
| None -> NoMoreElements |

284 |
end |

285 | |

286 |
let rec listFromLazylist evalfunc = |

287 |
let step = evalfunc () in |

288 |
match step with |

289 |
| NoMoreElements -> [] |

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

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

292 | |

293 |
type nominal = sort * localFormula |

294 | |

295 |
type node = |

296 |
| State of state |

297 |
| Core of core |

298 | |

299 |
type constrnt = |

300 |
| UnsatC |

301 |
| SatC |

302 |
| OpenC of node list |

303 |
| UnexpandedC of node list |

304 | |

305 |
type propagateElement = |

306 |
| UState of state * int option |

307 |
| UCore of core * bool |

308 |
| UCnstr of cset |

309 | |

310 |
type queueElement = |

311 |
| QState of state |

312 |
| QCore of core |

313 |
| QCnstr of cset |

314 |
| QEmpty |

315 | |

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

317 | |

318 |
exception CoAlg_finished of bool |

319 | |

320 | |

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

322 | |

323 |
let junctionEvalBool : (bool list junction) -> bool = function |

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

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

326 | |

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

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

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

330 | |

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

332 |
match x with |

333 |
| None -> None |

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

335 |
| None -> None |

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

337 | |

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

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

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

341 |
then extreme |

342 |
else optionalizeOperator op x y |

343 |
in function |

344 |
| Disjunctive l -> |

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

346 |
| Conjunctive l -> |

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

348 | |

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

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

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

352 | |

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

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

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

356 | |

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

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

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

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

361 |
let doPropagation = ref false |

362 | |

363 |
let queueInit () = |

364 |
queueStates := []; |

365 |
queueCores1 := []; |

366 |
queueCores2 := []; |

367 |
queueCnstrs := []; |

368 |
doPropagation := false |

369 | |

370 |
let queueIsEmpty () = |

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

372 | |

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

374 | |

375 |
(* original version: breadth-first *) |

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

377 | |

378 |
(* experiment: depth first |

379 |
let queueInsertCore core = queueCores1 := core::!queueCores1 |

380 |
*) |

381 | |

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

383 | |

384 |
let queueGetElement () = |

385 |
if !queueCnstrs <> [] then |

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

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

388 |
QCnstr res |

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

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

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

392 |
QState res |

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

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

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

396 |
QCore res |

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

398 |
else |

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

400 |
doPropagation := true; |

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

402 |
queueCores2 := []; |

403 |
QCore res |

404 | |

405 |
let doNominalPropagation () = !doPropagation |

406 | |

407 |
let doSatPropagation () = |

408 |
let res = !doPropagation in |

409 |
doPropagation := false; |

410 |
res |

411 | |

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

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

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

415 | |

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

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

418 |
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t) |

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

420 | |

421 |
let graphInit () = |

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

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

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

425 |
graphCnstrs := GHtS.create 128; |

426 |
graphRoot := None |

427 | |

428 |
let graphIterStates fkt = |

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

430 | |

431 |
let graphIterCores fkt = |

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

433 | |

434 |
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs |

435 | |

436 |
let graphClearCnstr () = |

437 |
let newGraph = GHtS.create (GHtS.length !graphCnstrs) in |

438 |
let copyCnstr cset cnstr = |

439 |
match cnstr with |

440 |
| UnsatC |

441 |
| SatC -> GHtS.add newGraph cset cnstr |

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

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

444 |
in |

445 |
GHtS.iter copyCnstr !graphCnstrs; |

446 |
graphCnstrs := newGraph |

447 | |

448 |
let graphFindState sort bs = |

449 |
try |

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

451 |
with Not_found -> None |

452 | |

453 |
let graphFindCore sort bs = |

454 |
try |

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

456 |
with Not_found -> None |

457 | |

458 |
let graphFindCnstr cset = |

459 |
try |

460 |
Some (GHtS.find !graphCnstrs cset) |

461 |
with Not_found -> None |

462 | |

463 |
let graphInsertState sort bs state = |

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

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

466 | |

467 |
let graphInsertCore sort bs core = |

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

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

470 | |

471 |
let graphInsertCnstr cset cnstr = |

472 |
assert (not (GHtS.mem !graphCnstrs cset)); |

473 |
GHtS.add !graphCnstrs cset cnstr |

474 | |

475 |
let graphReplaceCnstr cset cnstr = |

476 |
GHtS.replace !graphCnstrs cset cnstr |

477 | |

478 |
let graphSizeState () = |

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

480 |
let graphSizeCore () = |

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

482 |
let graphSizeCnstr () = GHtS.length !graphCnstrs |

483 | |

484 |
let graphAddRoot core = |

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

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

487 | |

488 |
let graphGetRoot () = |

489 |
match !graphRoot with |

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

491 |
| Some core -> core |

492 | |

493 | |

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

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

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

497 | |

498 |
let cssEmpty = BsSet.empty |

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

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

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

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

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

504 |
let cssSingleton cset = BsSet.singleton cset |

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

506 |
let cssIter (action: cset -> unit) css = |

507 |
BsSet.iter action css |

508 | |

509 | |

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

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

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

513 |
let nodeCounter = ref 0 |

514 |
let nextNodeIdx () : int = |

515 |
let oldVal = !nodeCounter in |

516 |
nodeCounter := oldVal + 1; |

517 |
oldVal |

518 | |

519 |
let stateMake sort bs defer exp = |

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

521 |
constraintsS = cssEmpty; expandFkt = exp; |

522 |
idx = nextNodeIdx() |

523 |
} |

524 |
let stateGetSort state = state.sortS |

525 |
let stateGetBs state = state.bsS |

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

527 |
let stateGetDeferral state = state.deferralS |

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

529 |
let stateGetStatus state = state.statusS |

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

531 |
let stateGetParents state = state.parentsS |

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

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

534 |
let stateGetRules state = state.childrenS |

535 |
let stateAddRule state dep children = |

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

537 |
List.length state.childrenS |

538 |
let stateGetConstraints state = state.constraintsS |

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

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

541 |
let stateGetIdx (state:state) = state.idx |

542 | |

543 | |

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

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

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

547 | |

548 |
let coreMake sort bs defer solver fht = |

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

550 |
constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = []; |

551 |
idx = nextNodeIdx() |

552 |
} |

553 |
let coreGetSort core = core.sortC |

554 |
let coreGetBs core = core.bsC |

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

556 |
let coreGetDeferral core = core.deferralC |

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

558 |
let coreGetStatus core = core.statusC |

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

560 |
let coreGetParents core = core.parentsC |

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

562 |
let coreGetChildren core = core.childrenC |

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

564 |
let coreGetConstraints core = core.constraintsC |

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

566 |
let coreGetSolver core = core.solver |

567 |
let coreGetFht core = core.fht |

568 |
let coreGetIdx (core:core) = core.idx |

569 |
let coreGetConstraintParents core = core.constraintParents |

570 |
let coreAddConstraintParent core cset = |

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

572 | |

573 | |

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

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

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

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

578 | |

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

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

581 |
let setEmptyCnstr () = GHtS.create 128 |

582 |
let setAddState set state = |

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

584 |
let setAddCore set core = |

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

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

587 |
let setMemState set state = |

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

589 |
let setMemCore set core = |

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

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

592 |
let setRemoveState set state = |

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

594 |
let setRemoveCore set core = |

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

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

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

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

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

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

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

602 | |

603 | |

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

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

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

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

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

609 | |

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

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

612 |
let lhtFind lht lit = |

613 |
try |

614 |
Some (LHt.find lht lit) |

615 |
with Not_found -> None |

616 | |

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

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

619 |
let fhtFind fht f = |

620 |
try |

621 |
Some (FHt.find fht f) |

622 |
with Not_found -> None |

623 | |

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

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

626 |
let nhtFind nht nom = |

627 |
try |

628 |
Some (NHt.find nht nom) |

629 |
with Not_found -> None |

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

631 | |

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

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

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

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

636 | |

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

638 | |

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

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

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

642 |
let bsetRem bs lf = S.remBS bs lf |

643 |
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2 |

644 |
let bsetMakeRealEmpty () = |

645 |
let res = bsetMake () in |

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

647 |
res |

648 |
let bsetCopy bs = S.copyBS bs |

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

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

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

652 |
let res = bsetMakeRealEmpty () in |

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

654 |
res |

655 | |

656 |
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort) |

657 | |

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

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

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

661 |
let csetCopy cs = S.copyBS cs |

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

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

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

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

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

667 |
let csetIter cs fkt = |

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

669 |
S.iterBS fkt2 cs |

670 | |

671 | |

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

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

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

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

676 | |

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

678 |
*) |

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

680 | |

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

682 |
*) |

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

684 | |

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

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

687 |
*) |

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

689 | |

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

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

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

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

694 |
*) |

695 |
(* |

696 |
for PML: arrayDest1 = the subformula |

697 |
arrayNum = the nominator of the probability |

698 |
arrayNum2 = the denominator of the probability |

699 |
*) |

700 |
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *) |

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

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

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

704 |
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *) |

705 |
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1))) (* another integer *) |

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

707 | |

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

709 |
to their @-wrapper. |

710 |
*) |

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

712 | |

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

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

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

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

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

718 |
let lfGetDestNum sort f = !arrayDestNum.(sort).(f) |

719 |
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f) |

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

721 |
let lfGetNeg sort f = |

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

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

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

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

726 |
let lfToInt lf = lf |

727 |
let lfFromInt num = num |

728 |
let lfGetFormula sort f = !arrayFormula.(sort).(f) |

729 | |

730 |
let escapeHtml (input : string) : string = |

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

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

733 |
input |

734 | |

735 |
let bsetToString sort bset : string = |

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

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

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

739 |
in |

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

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

742 | |

743 |
let csetToString sort cset = bsetToString sort cset |

744 | |

745 |
let coreToString (core:core): string = |

746 |
let helper cset lst : string list = |

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

748 |
in |

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

750 |
let children = |

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

752 |
in |

753 |
let parents = |

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

755 |
in |

756 |
"Core "^(string_of_int core.idx)^" {\n"^ |

757 |
" Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^ |

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

759 |
" Deferrals: \n" ^ |

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

761 |
" Constraints: { "^(String.concat |

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

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

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

765 |
" Parents: { "^(String.concat ", " parents)^" }\n"^ |

766 |
"}" |

767 | |

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

769 |
let helper cset lst : string list = |

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

771 |
in |

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

773 |
let core2idx core = core.idx in |

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

775 |
let conclusionList = |

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

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

778 |
) state.childrenS |

779 |
in |

780 |
let conclusionList = |

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

782 |
in |

783 |
let parents = |

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

785 |
in |

786 |
"State "^(string_of_int state.idx)^" {\n"^ |

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

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

789 |
" Deferrals: \n" ^ |

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

791 |
" Constraints: { "^(String.concat |

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

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

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

795 |
" Parents: { "^(String.concat ", " parents)^" }\n"^ |

796 |
"}" |

797 | |

798 |
let stateToDot (state:state): string = |

799 |
let color = match state.statusS with |

800 |
| Sat -> "green" |

801 |
| Unsat -> "red" |

802 |
| Open -> "yellow" |

803 |
| Expandable -> "white" |

804 |
in |

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

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

807 |
if (bsetMem state.deferralS lf) |

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

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

810 |
in |

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

812 |
let ownidx = (string_of_int state.idx) in |

813 |
let parents = |

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

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

816 |
state.parentsS |

817 |
in |

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

819 |
^ ",label=<State " ^ ownidx |

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

821 |
^ ">];\n" |

822 |
^ (String.concat "\n" parents) |

823 | |

824 | |

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

826 |
let color = match core.statusC with |

827 |
| Sat -> "green" |

828 |
| Unsat -> "red" |

829 |
| Open -> "yellow" |

830 |
| Expandable -> "white" |

831 |
in |

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

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

834 |
if (bsetMem core.deferralC lf) |

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

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

837 |
in |

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

839 |
let ownidx = (string_of_int core.idx) in |

840 |
let parents = |

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

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

843 |
core.parentsC |

844 |
in |

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

846 |
^ ",label=<Core " ^ ownidx |

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

848 |
^ ">];\n" |

849 |
^ (String.concat "\n" parents) |

850 | |

851 | |

852 |
let queuePrettyStatus () = |

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

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

855 |
in |

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

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

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

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

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

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

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

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

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

865 |
^"\n" |

866 | |

867 | |

868 | |

869 | |

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

871 |
let atFormulaGetNominal f = |

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

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

874 |
(s, n) |

875 | |

876 |
let lfToAt _ lf = lf |

877 | |

878 |
(* Calculate all possible formulae. This includes all subformulae and |

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

880 | |

881 |
TODO: variable sort needs to match epected sort |

882 |
*) |

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

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

885 |
let detClosure_ = detClosure newvars in |

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

887 |
then (List.hd newvars) |

888 |
else "ε" in |

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

890 |
let sstr = string_of_int s in |

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

892 |
else (); |

893 |
if C.HcFHt.mem vset.(s) f && |

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

895 |
else |

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

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

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

899 |
match f.HC.node with |

900 |
| C.HCTRUE |

901 |
| C.HCFALSE |

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

903 |
| C.HCAP name -> |

904 |
if C.isNominal name then begin |

905 |
Hashtbl.replace nomset name s; |

906 |
match nomTbl name with |

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

908 |
| Some sort -> |

909 |
if sort <> s then |

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

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

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

913 |
else () |

914 |
end else () |

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

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

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

918 |
let s1 = |

919 |
match nomTbl name with |

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

921 |
| Some sort -> sort |

922 |
in |

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

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

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

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

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

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

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

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

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

932 |
if (func <> MultiModalK && func <> MultiModalKD) |

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

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

935 |
else (); |

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

937 |
| C.HCENFORCES (_, f1) |

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

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

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

941 |
else (); |

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

943 |
| C.HCMORETHAN (_,_,f1) |

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

945 |
if func <> GML || List.length sortlst <> 1 |

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

947 |
else (); |

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

949 |
| C.HCATLEASTPROB (_,f1) |

950 |
| C.HCLESSPROBFAIL (_,f1) -> |

951 |
if func <> PML || List.length sortlst <> 1 |

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

953 |
else (); |

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

955 |
(* |

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

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

958 |
*) |

959 |
| C.HCCONST color |

960 |
| C.HCCONSTN color -> |

961 |
begin match func with |

962 |
| Constant params -> |

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

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

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

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

967 |
end; |

968 |
if List.length sortlst <> 1 |

969 |
then raise (C.CoAlgException "=-formula is used in wrong sort.") |

970 |
else (); |

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

972 |
| C.HCID f1 -> |

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

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

975 |
formula of wrong sort.") |

976 |
else (); |

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

978 |
| C.HCNORM (f1, f2) |

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

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

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

982 |
formulae of wrong sort.") |

983 |
else (); |

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

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

986 | |

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

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

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

990 |
else (); |

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

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

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

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

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

996 |
else (); |

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

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

999 |
(* |

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

1001 |
*) |

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

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

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

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

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

1007 |
| C.HCNU (name, f1) -> |

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

1009 |
detClosure_ nomTbl hcF fset vset atset nomset s unfold |

1010 | |

1011 | |

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

1013 |
match f.HC.node with |

1014 |
| C.HCTRUE |

1015 |
| C.HCFALSE |

1016 |
| C.HCOR _ |

1017 |
| C.HCAND _ |

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

1019 |
| _ -> |

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

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

1022 | |

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

1024 |
*) |

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

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

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

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

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

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

1031 |
match f.HC.node with |

1032 |
| C.HCTRUE |

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

1034 |
| C.HCAP name -> |

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

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

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

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

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

1040 |
let s1 = |

1041 |
match nomTbl name with |

1042 |
| None -> assert false |

1043 |
| Some sort -> sort |

1044 |
in |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1062 |
else |

1063 |
let size = Hashtbl.length htR in |

1064 |
Hashtbl.add htR role size; |

1065 |
size |

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

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

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

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

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

1071 |
else |

1072 |
let size = Hashtbl.length htR in |

1073 |
Hashtbl.add htR role size; |

1074 |
size |

1075 |
| C.HCENFORCES (aglist, f1) -> (* aglist = list of agents *) |

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

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

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

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

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

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

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

1083 |
| C.HCMORETHAN (cnt,role,f1) -> |

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

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

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

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

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

1089 |
else |

1090 |
let size = Hashtbl.length htR in |

1091 |
Hashtbl.add htR role size; |

1092 |
size |

1093 |
| C.HCMAXEXCEPT (cnt,role,f1) -> |

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

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

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

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

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

1099 |
else |

1100 |
let size = Hashtbl.length htR in |

1101 |
Hashtbl.add htR role size; |

1102 |
size |

1103 |
| C.HCATLEASTPROB (p,f1) -> |

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

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

1106 |
!arrayDestNum.(s).(n) <- p.C.nominator; |

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

1108 |
| C.HCLESSPROBFAIL (p,f1) -> |

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

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

1111 |
!arrayDestNum.(s).(n) <- p.C.nominator; |

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

1113 |
| C.HCCONST str -> |

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

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

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

1117 |
fractions, here: none *) |

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

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

1120 |
else |

1121 |
let size = Hashtbl.length htR in |

1122 |
Hashtbl.add htR str size; |

1123 |
size |

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

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

1126 |
| C.HCCONSTN str -> |

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

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

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

1130 |
fractions, here: none *) |

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

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

1133 |
else |

1134 |
let size = Hashtbl.length htR in |

1135 |
Hashtbl.add htR str size; |

1136 |
size |

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

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

1139 |
| C.HCID (f1) -> |

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

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

1142 |
| C.HCNORM (f1, f2) -> |

1143 |
!arrayType.(s).(n) <- NormF; |

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

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

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

1147 |
!arrayType.(s).(n) <- NormnF; |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1164 |
| C.HCNU (name, f1) -> |

1165 |
!arrayType.(s).(n) <- NuF; |

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

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

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

1169 | |

1170 | |

1171 |
let initTablesAt hcF htF name sort = |

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

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

1174 |
let addAt f n = |

1175 |
match f.HC.node with |

1176 |
| C.HCTRUE |

1177 |
| C.HCFALSE |

1178 |
| C.HCOR _ |

1179 |
| C.HCAND _ |

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

1181 |
| _ -> |

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

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

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

1185 |
in |

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

1187 | |

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

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

1190 |
if card <= 0 then |

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

1192 |
else (); |

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

1194 |
let f1 = nnfAndSimplify f in |

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

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

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

1198 | |

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

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

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

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

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

1204 |
let hcfalse = C.hc_formula hcF C.FALSE in |

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

1206 | |

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

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

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

1210 |
let nomset = Hashtbl.create 16 in |

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

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

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

1214 |
done; |

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

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

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

1218 |
hctbox; |

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

1220 |
nhctbox; |

1221 |
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset; |

1222 | |

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

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

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

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

1227 |
done; |

1228 |
let addAts f () idx = |

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

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

1231 |
done; |

1232 |
idx + 1 |

1233 |
in |

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

1235 |
let addFml i f () idx = |

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

1237 |
else begin |

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

1239 |
idx+1 |

1240 |
end |

1241 |
in |

1242 |
let size = ref 0 in |

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

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

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

1246 |
done; |

1247 | |

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

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

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

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

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

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

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

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

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

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

1258 |
let htR = Hashtbl.create 128 in |

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

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

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

1262 | |

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

1264 |
let initbs = bsetMake () in |

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

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

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

1268 |
tboxTable := tboxTbl; |

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