## cool / src / lib / CoAlgReasoner.ml @ e4faff97

History | View | Annotate | Download (38.8 KB)

1 |
(** A graph-tableau-based decision procedure framework for coalgebraic logics. |
---|---|

2 |
@author Florian Widmann |

3 |
*) |

4 | |

5 | |

6 |
open CoAlgMisc |

7 | |

8 |
module M = Minisat |

9 | |

10 |
module CU = CoolUtils |

11 | |

12 |
type sortTable = CoAlgMisc.sortTable |

13 | |

14 |
type nomTable = string -> CoAlgFormula.sort option |

15 | |

16 |
type assumptions = CoAlgFormula.sortedFormula list |

17 | |

18 |
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula |

19 | |

20 |
exception ReasonerError of string |

21 | |

22 |
(*****************************************************************************) |

23 |
(* Propagation of Satisfiability *) |

24 |
(*****************************************************************************) |

25 | |

26 |
let propSatFindSucc setCnstr cset = |

27 |
if csetHasDot cset then false |

28 |
else |

29 |
match graphFindCnstr cset with |

30 |
| None -> raise (ReasonerError "?") |

31 |
| Some SatC -> true |

32 |
| Some (OpenC _) -> setMemCnstr setCnstr cset |

33 |
| Some (UnexpandedC _) |

34 |
| Some UnsatC -> false |

35 | |

36 | |

37 |
let rec propSat setStates setCores setCnstr = function |

38 |
| [] -> () |

39 |
| propElem::tl -> |

40 |
let tl1 = |

41 |
match propElem with |

42 |
| UState (state, _) -> |

43 |
if setMemState setStates state then |

44 |
let cnstrs = stateGetConstraints state in |

45 |
let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in |

46 |
if isStillOpen then () else setRemoveState setStates state |

47 |
else (); |

48 |
tl |

49 |
| UCore (core, _) -> |

50 |
if setMemCore setCores core then |

51 |
let cnstrs = coreGetConstraints core in |

52 |
let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in |

53 |
if isStillOpen then tl else begin |

54 |
setRemoveCore setCores core; |

55 |
let cnstrPar = coreGetConstraintParents core in |

56 |
List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl cnstrPar |

57 |
end |

58 |
else tl |

59 |
| UCnstr cset -> |

60 |
if setMemCnstr setCnstr cset then begin |

61 |
setRemoveCnstr setCnstr cset; |

62 |
match graphFindCnstr cset with |

63 |
| Some (OpenC nodes) -> |

64 |
let prop acc node = |

65 |
match node with |

66 |
| Core core -> (UCore (core, true))::acc |

67 |
| State state -> (UState (state, None))::acc |

68 |
in |

69 |
List.fold_left prop tl nodes |

70 |
| _ -> assert false |

71 |
end else tl |

72 |
in |

73 |
propSat setStates setCores setCnstr tl1 |

74 | |

75 |
let propagateSat () = |

76 |
let setStates = setEmptyState () in |

77 |
let setCores = setEmptyCore () in |

78 |
let setCnstr = setEmptyCnstr () in |

79 |
let fktS1 state = |

80 |
match stateGetStatus state with |

81 |
| Expandable |

82 |
| Open -> setAddState setStates state |

83 |
| Unsat |

84 |
| Sat -> () |

85 |
in |

86 |
graphIterStates fktS1; |

87 |
let fktC1 core = |

88 |
match coreGetStatus core with |

89 |
| Expandable |

90 |
| Open -> setAddCore setCores core |

91 |
| Unsat |

92 |
| Sat -> () |

93 |
in |

94 |
graphIterCores fktC1; |

95 |
let cfkt1 cset cnstr = |

96 |
if csetHasDot cset then () |

97 |
else |

98 |
match cnstr with |

99 |
| OpenC _ -> setAddCnstr setCnstr cset |

100 |
| UnsatC |

101 |
| SatC |

102 |
| UnexpandedC _ -> () |

103 |
in |

104 |
graphIterCnstrs cfkt1; |

105 |
graphIterStates (fun state -> propSat setStates setCores setCnstr [UState (state, None)]); |

106 |
graphIterCores (fun core -> propSat setStates setCores setCnstr [UCore (core, false)]); |

107 |
setIterState (fun state -> stateSetStatus state Sat) setStates; |

108 |
let setCoreSat core = |

109 |
coreSetStatus core Sat; |

110 |
if core == graphGetRoot () then raise (CoAlg_finished true) else () |

111 |
in |

112 |
setIterCore setCoreSat setCores; |

113 |
setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr |

114 | |

115 | |

116 |
let propagateSatMu () = |

117 |
let setFinishingStates = setEmptyState () in |

118 |
let setFinishingCores = setEmptyCore () in |

119 |
let setStates = setEmptyState () in |

120 |
let setCores = setEmptyCore () in |

121 |
let emptySet = bsetMakeRealEmpty () in |

122 | |

123 |
(* Collect two sets of nodes. All nodes that may be satisfiable |

124 |
* after this iteration are collected into setStates/setCores. |

125 |
* |

126 |
* As every cycle containing a node with empty focus or an |

127 |
* satisfiable node should be considered satisfiable, collect these |

128 |
* decisive nodes into setFinishingStates/setFinishingCores |

129 |
* |

130 |
* This also marks in trivial cases nodes as satisfiable. |

131 |
*) |

132 |
let stateCollector state = |

133 |
match stateGetStatus state with |

134 |
| Unsat -> () |

135 |
| Sat -> |

136 |
setAddState setStates state; |

137 |
setAddState setFinishingStates state |

138 |
| Expandable -> () |

139 |
| Open -> |

140 |
if List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *) |

141 |
bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *) |

142 |
then begin |

143 |
setAddState setFinishingStates state; |

144 |
stateSetStatus state Sat |

145 |
end else begin |

146 |
setAddState setStates state; |

147 |
if bsetCompare (stateGetDeferral state) emptySet == 0 |

148 |
then begin |

149 |
print_endline (stateToString state); |

150 |
setAddState setFinishingStates state |

151 |
end |

152 |
else () |

153 |
end |

154 | |

155 |
(* As it is enough for a core to have one successfull child, we can |

156 |
* also handle (some) expandable cores. |

157 |
*) |

158 |
and coreCollector core = |

159 |
match coreGetStatus core with |

160 |
| Unsat -> () |

161 |
| Sat -> |

162 |
setAddCore setCores core; |

163 |
setAddCore setFinishingCores core |

164 |
| Expandable |

165 |
| Open -> |

166 |
setAddCore setCores core; |

167 |
if bsetCompare (coreGetDeferral core) emptySet == 0 |

168 |
then begin |

169 |
print_endline (coreToString core); |

170 |
setAddCore setFinishingCores core |

171 |
end |

172 |
else () |

173 |
in |

174 |
graphIterStates stateCollector; |

175 |
graphIterCores coreCollector; |

176 | |

177 |
(* In a fixpoint the set called setStates / setCores is narrowed |

178 |
* down. |

179 |
* |

180 |
* In each step only those states and cores are retained in setStates |

181 |
* / setCores which reach one of setFinishing{States,Cores} in |

182 |
* finitely many steps. This new set of States / Cores is collected |

183 |
* as allowed{States,Cores} during each fixpoint iteration. |

184 |
* |

185 |
* Only those finishing nodes are retained that have allowed or |

186 |
* Successfull Children. |

187 |
*) |

188 |
let rec fixpointstep setStates setCores = |

189 |
let allowedStates = setEmptyState () in |

190 |
let allowedCores = setEmptyCore () in |

191 | |

192 |
let rec visitParentStates (core : core) : unit = |

193 |
print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core))); |

194 |
if not (setMemCore allowedCores core) |

195 |
then begin |

196 |
setAddCore allowedCores core; |

197 |
print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core))); |

198 |
let verifyParent (state,_) = |

199 |
let rules = stateGetRules state in |

200 |
let ruleiter (dependencies, corelist) = |

201 |
List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat) |

202 |
corelist |

203 |
in |

204 |
if List.for_all ruleiter rules |

205 |
then visitParentCores state |

206 |
else print_endline ("Not considering state "^(string_of_int (stateGetIdx state))) |

207 |
in |

208 |
List.iter verifyParent (coreGetParents core) |

209 |
end |

210 | |

211 |
and visitParentCores (state : state) : unit = |

212 |
print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state))); |

213 |
if not (setMemState allowedStates state) |

214 |
then begin |

215 |
setAddState allowedStates state; |

216 |
print_endline ("Adding State " ^ (string_of_int (stateGetIdx state))); |

217 |
let verifyParent core = |

218 |
let acceptable = |

219 |
List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat) |

220 |
(coreGetChildren core) |

221 |
in |

222 |
if acceptable |

223 |
then visitParentStates core |

224 |
else print_endline ("Not considering state "^(string_of_int (coreGetIdx core))) |

225 |
in |

226 |
List.iter verifyParent (stateGetParents state) |

227 |
end |

228 |
in |

229 | |

230 |
(* All rule applications need to still be potentially Sat for a |

231 |
* finishing State to be a valid startingpoint for this fixpoint. |

232 |
*) |

233 |
let checkFinishingState (state : state) = |

234 |
let ruleiter (dependencies, corelist) : bool = |

235 |
List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist |

236 |
in |

237 |
if not (List.exists ruleiter (stateGetRules state)) then begin |

238 |
print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node"); |

239 |
visitParentCores state |

240 |
end |

241 | |

242 |
(* There needs to be a State still potentially Sat for this core |

243 |
* to be considered for the fixpoint |

244 |
*) |

245 |
and checkFinishingCore (core : core) = |

246 |
if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state)) |

247 |
(coreGetChildren core)) |

248 |
then begin |

249 |
print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node"); |

250 |
visitParentStates core |

251 |
end |

252 |
in |

253 |
setIterState checkFinishingState setFinishingStates; |

254 |
setIterCore checkFinishingCore setFinishingCores; |

255 | |

256 | |

257 |
if (setLengthState setStates) = (setLengthState allowedStates) && |

258 |
(setLengthCore setCores) = (setLengthCore allowedCores) |

259 |
then begin |

260 |
setIterState (fun state -> stateSetStatus state Sat) setStates; |

261 |
setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores; |

262 |
end else |

263 |
fixpointstep allowedStates allowedCores |

264 |
in |

265 |
fixpointstep setStates setCores |

266 | |

267 | |

268 |
(*****************************************************************************) |

269 |
(* Propagation of Unsatisfiability *) |

270 |
(*****************************************************************************) |

271 | |

272 |
let isConstraintUnsat cset = |

273 |
match graphFindCnstr cset with |

274 |
| None -> assert false |

275 |
| Some UnsatC -> true |

276 |
| _ -> false |

277 | |

278 |
let fhtMustFind fht f = |

279 |
match fhtFind fht f with |

280 |
| Some l -> l |

281 |
| None -> assert false |

282 | |

283 |
let lhtMustFind lht l = |

284 |
match lhtFind lht l with |

285 |
| Some f -> f |

286 |
| None -> assert false |

287 | |

288 | |

289 |
(* Gets a list of Things we know are unsatisfiable and propagates this |

290 |
information backwards *) |

291 |
let rec propagateUnsat = function |

292 |
| [] -> () |

293 |
| propElem::tl -> |

294 |
let tl1 = |

295 |
match propElem with |

296 |
| UState (state, idxopt) -> begin |

297 |
match stateGetStatus state with |

298 |
| Unsat -> tl |

299 |
| Sat -> raise (ReasonerError ("Propagation tells state " |

300 |
^(string_of_int (stateGetIdx state)) |

301 |
^" would be unsat, but it is already sat")) |

302 |
| Open |

303 |
| Expandable -> |

304 |
let mbs = |

305 |
match idxopt with |

306 |
| None -> stateGetBs state |

307 |
| Some idx -> |

308 |
let (dep, children) = stateGetRule state idx in |

309 |
let getBs core = |

310 |
assert (coreGetStatus core = Unsat); |

311 |
coreGetBs core |

312 |
in |

313 |
dep (List.map getBs children) |

314 |
in |

315 |
stateSetBs state mbs; |

316 |
stateSetStatus state Unsat; |

317 |
let prop acc core = |

318 |
let turnsUnsat = |

319 |
match coreGetStatus core with |

320 |
| Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) |

321 |
| Expandable |

322 |
| Unsat |

323 |
| Sat -> false |

324 |
in |

325 |
if turnsUnsat then (UCore (core, false))::acc else acc |

326 |
in |

327 |
List.fold_left prop tl (stateGetParents state) |

328 |
end |

329 |
| UCore (core, comesFromCnstr) -> begin |

330 |
match coreGetStatus core with |

331 |
| Unsat -> tl |

332 |
| Sat -> raise (ReasonerError ("Propagation tells core " |

333 |
^(string_of_int (coreGetIdx core)) |

334 |
^" would be unsat, but it is already sat")) |

335 |
| Open |

336 |
| Expandable -> |

337 |
let mbs = |

338 |
if comesFromCnstr then coreGetBs core |

339 |
else |

340 |
let bs = coreGetBs core in |

341 |
let solver = coreGetSolver core in |

342 |
let fht = coreGetFht core in |

343 |
let lht = lhtInit () in |

344 |
let addLits f acc = |

345 |
let lit = fhtMustFind fht f in |

346 |
lhtAdd lht lit f; |

347 |
lit::acc |

348 |
in |

349 |
let litset = bsetFold addLits bs [] in |

350 |
let addClauses state = |

351 |
let cbs = stateGetBs state in |

352 |
let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in |

353 |
let okay = M.add_clause solver clause in |

354 |
assert okay |

355 |
in |

356 |
List.iter addClauses (coreGetChildren core); |

357 |
let isSat = M.invoke_solver solver litset in |

358 |
assert (not isSat); |

359 |
let res = bsetMake () in |

360 |
let confls = M.get_conflict solver in |

361 |
List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls; |

362 |
res |

363 |
in |

364 |
coreSetBs core mbs; |

365 |
coreSetStatus core Unsat; |

366 |
if core == graphGetRoot () then raise (CoAlg_finished false) else (); |

367 |
let prop acc (state, idx) = |

368 |
let turnsUnsat = |

369 |
match stateGetStatus state with |

370 |
| Open |

371 |
| Expandable -> |

372 |
List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx)) |

373 |
| Unsat |

374 |
| Sat -> false |

375 |
in |

376 |
if turnsUnsat then (UState (state, Some idx))::acc else acc |

377 |
in |

378 |
let tl2 = List.fold_left prop tl (coreGetParents core) in |

379 |
List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core) |

380 |
end |

381 |
| UCnstr cset -> |

382 |
match graphFindCnstr cset with |

383 |
| None |

384 |
| Some SatC -> assert false |

385 |
| Some UnsatC -> tl |

386 |
| Some (UnexpandedC nodes) |

387 |
| Some (OpenC nodes) -> |

388 |
graphReplaceCnstr cset UnsatC; |

389 |
let prop acc node = |

390 |
match node with |

391 |
| State state -> |

392 |
let turnsUnsat = |

393 |
match stateGetStatus state with |

394 |
| Expandable |

395 |
| Open -> cssForall isConstraintUnsat (stateGetConstraints state) |

396 |
| Unsat |

397 |
| Sat -> false |

398 |
in |

399 |
if turnsUnsat then (UState (state, None))::acc else acc |

400 |
| Core core -> |

401 |
let turnsUnsat = |

402 |
match coreGetStatus core with |

403 |
| Expandable |

404 |
| Open -> cssForall isConstraintUnsat (coreGetConstraints core) |

405 |
| Unsat |

406 |
| Sat -> false |

407 |
in |

408 |
if turnsUnsat then (UCore (core, true))::acc else acc |

409 |
in |

410 |
List.fold_left prop tl nodes |

411 |
in |

412 |
propagateUnsat tl1 |

413 | |

414 |
let propagateUnsatMu () = |

415 |
let setFinishingStates = setEmptyState () in |

416 |
let setFinishingCores = setEmptyCore () in |

417 |
let setStates = setEmptyState () in |

418 |
let setCores = setEmptyCore () in |

419 |
let emptySet = bsetMakeRealEmpty () in |

420 | |

421 |
(* Collect two sets of nodes. All nodes that may be unsatisfiable |

422 |
* after this iteration are collected into setStates/setCores. |

423 |
* |

424 |
* Nodes reaching Points with empty focus as well as Expandable nodes |

425 |
* (if not Unsat) can not be declared Unsat so we collect these into |

426 |
* setFinishingStates/setFinishingCores. |

427 |
*) |

428 |
let stateCollector state = |

429 |
match stateGetStatus state with |

430 |
| Unsat -> () |

431 |
| Sat |

432 |
| Expandable -> |

433 |
setAddState setStates state; |

434 |
setAddState setFinishingStates state |

435 |
| Open -> |

436 |
setAddState setStates state; |

437 |
if bsetCompare (stateGetDeferral state) emptySet == 0 |

438 |
then begin |

439 |
setAddState setFinishingStates state |

440 |
end |

441 |
else () |

442 | |

443 |
and coreCollector core = |

444 |
match coreGetStatus core with |

445 |
| Unsat -> () |

446 |
| Expandable |

447 |
| Sat -> |

448 |
setAddCore setCores core; |

449 |
setAddCore setFinishingCores core |

450 |
| Open -> |

451 |
setAddCore setCores core; |

452 |
if bsetCompare (coreGetDeferral core) emptySet == 0 |

453 |
then begin |

454 |
setAddCore setFinishingCores core |

455 |
end |

456 |
else () |

457 |
in |

458 |
graphIterStates stateCollector; |

459 |
graphIterCores coreCollector; |

460 | |

461 |
(* In a fixpoint the set called setFinishingStates/setFinishingCores |

462 |
* is narrowed down |

463 |
* |

464 |
* In each iteration we start with all Nodes and remove all that can |

465 |
* reach a finishing Node. We then remove all finishing Nodes from the |

466 |
* respective set which are becoming Unsat and start with the next |

467 |
* iteration until the fixpoint is reached |

468 |
* |

469 |
* |

470 |
*) |

471 |
let rec fixpointstep setPrevUnsatStates setPrevUnsatCores = |

472 |
let setUnsatStates = setCopyState setStates in |

473 |
let setUnsatCores = setCopyCore setCores in |

474 | |

475 |
let rec visitParentStates (core : core) : unit = |

476 |
if setMemCore setUnsatCores core |

477 |
then begin |

478 |
setRemoveCore setUnsatCores core; |

479 |
let verifyParent (state,_) = |

480 |
let rules = stateGetRules state in |

481 |
let ruleiter (dependencies, corelist) = |

482 |
List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat) |

483 |
corelist |

484 |
in |

485 |
if List.for_all ruleiter rules |

486 |
then visitParentCores state |

487 |
in |

488 |
List.iter verifyParent (coreGetParents core) |

489 |
end |

490 | |

491 |
and visitParentCores (state : state) : unit = |

492 |
if setMemState setUnsatStates state |

493 |
then begin |

494 |
setRemoveState setUnsatStates state; |

495 |
let verifyParent core = |

496 |
let acceptable = |

497 |
List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat) |

498 |
(coreGetChildren core) |

499 |
in |

500 |
if acceptable |

501 |
then visitParentStates core |

502 |
in |

503 |
List.iter verifyParent (stateGetParents state) |

504 |
end |

505 |
in |

506 | |

507 |
(* All rule applications need to still be potentially Sat for a |

508 |
* finishing State to be a valid startingpoint for this fixpoint. |

509 |
*) |

510 |
let checkFinishingState (state : state) = |

511 |
let ruleiter (dependencies, corelist) : bool = |

512 |
List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist |

513 |
in |

514 |
if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin |

515 |
visitParentCores state |

516 |
end |

517 | |

518 |
(* There needs to be a State still potentially Sat for this core |

519 |
* to be considered for the fixpoint |

520 |
*) |

521 |
and checkFinishingCore (core : core) = |

522 |
if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state) |

523 |
(coreGetChildren core)) || |

524 |
coreGetStatus core == Expandable |

525 |
then begin |

526 |
visitParentStates core |

527 |
end |

528 |
in |

529 |
setIterState checkFinishingState setFinishingStates; |

530 |
setIterCore checkFinishingCore setFinishingCores; |

531 | |

532 |
if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) && |

533 |
(setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores) |

534 |
then begin |

535 |
setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates; |

536 |
setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores; |

537 |
end else |

538 |
fixpointstep setUnsatStates setUnsatCores |

539 |
in |

540 |
fixpointstep (setEmptyState ()) (setEmptyCore ()) |

541 | |

542 | |

543 |
(*****************************************************************************) |

544 |
(* Propagation of Nominal Constraints *) |

545 |
(*****************************************************************************) |

546 | |

547 |
let extractAts sort bs = |

548 |
let ats = csetMake () in |

549 |
let procNom nom f = |

550 |
match lfGetType sort f with |

551 |
| AndF |

552 |
| OrF -> () |

553 |
| TrueFalseF |

554 |
| AtF -> () |

555 |
| _ -> csetAdd ats (lfGetAt (sort, nom) f) |

556 |
in |

557 |
let getAts f = |

558 |
match lfGetType sort f with |

559 |
| AtF -> csetAdd ats (lfToAt sort f) |

560 |
| NomF -> bsetIter (fun f1 -> procNom f f1) bs |

561 |
| _ -> () |

562 |
in |

563 |
bsetIter getAts bs; |

564 |
ats |

565 | |

566 |
let detConstraintsState state = |

567 |
let procRule accR (_, chldrn) = |

568 |
let procChldrn accC core = |

569 |
if coreGetStatus core = Unsat then accC |

570 |
else cssUnion accC (coreGetConstraints core) |

571 |
in |

572 |
let orset = List.fold_left procChldrn cssEmpty chldrn in |

573 |
let procOrset csetO accO = |

574 |
let mkUnion csetU accU = |

575 |
let cset = csetUnion csetO csetU in |

576 |
cssAdd cset accU |

577 |
in |

578 |
cssFold mkUnion accR accO |

579 |
in |

580 |
cssFold procOrset orset cssEmpty |

581 |
in |

582 |
let sort = stateGetSort state in |

583 |
let bs = stateGetBs state in |

584 |
let ats = extractAts sort bs in |

585 |
if stateGetStatus state = Expandable then csetAddDot ats else (); |

586 |
List.fold_left procRule (cssSingleton ats) (stateGetRules state) |

587 | |

588 |
let detConstraintsCore core = |

589 |
let sort = coreGetSort core in |

590 |
let bs = coreGetBs core in |

591 |
let ats = extractAts sort bs in |

592 |
let addCnstr acc state = |

593 |
if stateGetStatus state = Unsat then acc |

594 |
else |

595 |
let csets = stateGetConstraints state in |

596 |
(* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *) |

597 |
cssUnion csets acc |

598 |
in |

599 |
let initInner = |

600 |
if coreGetStatus core = Expandable then |

601 |
(* let cset = csetCopy ats in *) |

602 |
let cset = ats in |

603 |
csetAddDot cset; |

604 |
cssSingleton cset |

605 |
else cssEmpty |

606 |
in |

607 |
List.fold_left addCnstr initInner (coreGetChildren core) |

608 | |

609 |
let rec propNom = function |

610 |
| [] -> () |

611 |
| node::tl -> |

612 |
let tl1 = |

613 |
match node with |

614 |
| State state -> |

615 |
if stateGetStatus state = Unsat then tl |

616 |
else |

617 |
let csets = detConstraintsState state in |

618 |
let oldcsets = stateGetConstraints state in |

619 |
if cssEqual csets oldcsets then tl |

620 |
else begin |

621 |
stateSetConstraints state csets; |

622 |
List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state) |

623 |
end |

624 |
| Core core -> |

625 |
if coreGetStatus core = Unsat then tl |

626 |
else |

627 |
let csets = detConstraintsCore core in |

628 |
let oldcsets = coreGetConstraints core in |

629 |
if cssEqual csets oldcsets then tl |

630 |
else begin |

631 |
coreSetConstraints core csets; |

632 |
List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core) |

633 |
end |

634 |
in |

635 |
propNom tl1 |

636 | |

637 |
let updateConstraints node elemU csets = |

638 |
let update cset acc = |

639 |
let cnstr = |

640 |
match graphFindCnstr cset with |

641 |
| Some cn -> cn |

642 |
| None -> |

643 |
let cn = UnexpandedC [] in |

644 |
graphInsertCnstr cset cn; |

645 |
queueInsertCnstr cset; |

646 |
cn |

647 |
in |

648 |
match cnstr with |

649 |
| UnsatC -> acc |

650 |
| UnexpandedC parents -> |

651 |
graphReplaceCnstr cset (UnexpandedC (node::parents)); |

652 |
false |

653 |
| OpenC parents -> |

654 |
graphReplaceCnstr cset (OpenC (node::parents)); |

655 |
false |

656 |
| SatC -> false |

657 |
in |

658 |
let isUnsat = cssFold update csets true in |

659 |
if isUnsat then propagateUnsat [elemU] else () |

660 | |

661 |
let propagateNominals () = |

662 |
let init = cssSingleton (csetMake ()) in |

663 |
graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init); |

664 |
graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init); |

665 |
graphIterStates (fun s -> propNom [State s]); |

666 |
graphIterCores (fun c -> propNom [Core c]); |

667 |
graphClearCnstr (); |

668 |
let fktS state = |

669 |
if stateGetStatus state = Unsat then () |

670 |
else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state) |

671 |
in |

672 |
graphIterStates fktS; |

673 |
let fktC core = |

674 |
if coreGetStatus core = Unsat then () |

675 |
else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core) |

676 |
in |

677 |
graphIterCores fktC |

678 | |

679 | |

680 |
(*****************************************************************************) |

681 |
(* Node Expansions *) |

682 |
(*****************************************************************************) |

683 | |

684 |
let getLit sort fht solver f = |

685 |
match fhtFind fht f with |

686 |
| Some lit -> lit |

687 |
| None -> |

688 |
let var = M.new_variable solver in |

689 |
let lit = M.var_to_lit var true in |

690 |
fhtAdd fht f lit; |

691 |
let () = |

692 |
match lfGetNeg sort f with |

693 |
| None -> () |

694 |
| Some nf -> |

695 |
let nlit = M.neg_lit lit in |

696 |
fhtAdd fht nf nlit; |

697 |
in |

698 |
lit |

699 | |

700 |
let newCore sort bs defer = |

701 |
(* when creating a now core from a set of formulas bs |

702 |
bs = { x_1, ...., x_n } |

703 |
= "x_1 /\ .... /\ x_n" |

704 |
Then we do this by: |

705 | |

706 |
1. creating a new literal in the sat solver for each |

707 |
"boolean subformula" from the x_i. "boolean subformula" means that |

708 |
this subformula is not hidden under modalities but only under |

709 |
boolean connectives (/\, \/). |

710 |
2. encoding the relation between a formula and its intermediate boolean |

711 |
subformulas by a clause: |

712 |
*) |

713 |
let fht = fhtInit () in |

714 |
let solver = M.new_solver () in |

715 |
let rec addClauses f = |

716 |
(* step 1: create a literal in the satsolver representing the formula f *) |

717 |
let lf = getLit sort fht solver f in |

718 |
(* step 2: encode relation to possible subformulas *) |

719 |
match lfGetType sort f with |

720 |
| OrF -> |

721 |
(* |

722 |
case 2.(a) f = f1 \/ f2 |

723 |
fill fht such that it says: |

724 | |

725 |
f |---> lf |

726 |
f1 |---> lf1 |

727 |
f2 |---> lf2 |

728 |
*) |

729 |
let f1 = lfGetDest1 sort f in |

730 |
let f2 = lfGetDest2 sort f in |

731 |
addClauses f1; |

732 |
addClauses f2; |

733 |
let lf1 = fhtMustFind fht f1 in |

734 |
let lf2 = fhtMustFind fht f2 in |

735 |
(* |

736 |
encode the structure of f by adding the clause (lf -> lf1 \/ lf2) |

737 |
*) |

738 |
let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in |

739 |
assert (okay) |

740 |
| AndF -> |

741 |
(* |

742 |
case 2.(b) f = f1 /\ f2 |

743 |
fill fht such that it says: |

744 | |

745 |
f |---> lf |

746 |
f1 |---> lf1 |

747 |
f2 |---> lf2 |

748 |
*) |

749 |
let f1 = lfGetDest1 sort f in |

750 |
let f2 = lfGetDest2 sort f in |

751 |
addClauses f1; |

752 |
addClauses f2; |

753 |
let lf1 = fhtMustFind fht f1 in |

754 |
let lf2 = fhtMustFind fht f2 in |

755 |
(* |

756 |
encode the structure of f by adding the clauses |

757 |
(lf -> lf1) /\ (lf -> lf2) |

758 |
*) |

759 |
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in |

760 |
assert (okay1); |

761 |
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in |

762 |
assert (okay2) |

763 |
| MuF |

764 |
| NuF -> |

765 |
(* |

766 |
Dest of a fixpoint is it's unfolded version. This adds just |

767 |
an simple forward implication that could be optimised out |

768 |
though not without nontrivial transformation of code |

769 | |

770 |
f = μ X . φ |---> lf |

771 |
φ[X |-> f] |---> lf1 |

772 | |

773 |
Then adding lf -> lf1 to minisat |

774 |
*) |

775 |
let f1 = lfGetDest1 sort f in |

776 |
addClauses f1; |

777 |
let lf1 = fhtMustFind fht f1 in |

778 |
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in |

779 |
assert (okay1); |

780 |
| _ -> () |

781 |
(* case 2.(c) |

782 |
We don't need to do anything except adding f to the fht |

783 |
*) |

784 |
in |

785 |
bsetIter addClauses bs; |

786 |
coreMake sort bs defer solver fht |

787 | |

788 |
let getNextState core = |

789 |
(* Create a new state, which is obtained by a satisfying assignment of the |

790 |
literals of the minisat solver. |

791 |
In addition to that, feed the negation of the satisfying assignment back |

792 |
to the minisat solver in order to obtain different solutions on successive |

793 |
minisat calls. |

794 |
*) |

795 |
let bs = coreGetBs core in |

796 |
let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in |

797 |
let deferralS = |

798 |
if refocusing then |

799 |
bsetCopy bs |

800 |
else |

801 |
coreGetDeferral core |

802 |
in |

803 |
let fht = coreGetFht core in |

804 |
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in |

805 |
let solver = coreGetSolver core in |

806 |
let isSat = M.invoke_solver solver litset in |

807 |
(* Clearly, if the current core is unsatisfiable, no further child state can |

808 |
be created *) |

809 |
if not isSat then None |

810 |
else |

811 |
let sort = coreGetSort core in |

812 |
(* create a new set of formulas newbs with the property: |

813 |
if the conjunction of newbs is satisfiable, then the present core is |

814 |
satisfiable. |

815 |
*) |

816 |
let newbs = bsetMake () in |

817 |
let newdefer = bsetMakeRealEmpty () in |

818 |
(* if newbs = { l_1, .... l_n }, i.e. |

819 | |

820 |
newbs = l_1 /\ ... /\ l_n |

821 | |

822 |
then we can get essentially different satisfying assignments of bs by |

823 |
adding another clause |

824 | |

825 |
clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n |

826 | |

827 |
By mkExclClause, newbs is filled, and clause is built in the accumulator acc. |

828 |
*) |

829 |
let rec mkExclClause deferral f acc = |

830 |
(* f is a formula that is true in the current satisfying assignment *) |

831 |
match lfGetType sort f with |

832 |
| OrF -> |

833 |
(* if f is true and a disjunction, then one of its disjuncts is true *) |

834 |
let f1 = lfGetDest1 sort f in |

835 |
let lf1 = fhtMustFind fht f1 in |

836 |
(* if the first disjunct f1 is true, then we need to add subformulas |

837 |
of f1 to newbs&clause *) |

838 |
if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc |

839 |
else |

840 |
(* otherwise f2 must be true *) |

841 |
let f2 = lfGetDest2 sort f in |

842 |
let lf2 = fhtMustFind fht f2 in |

843 |
assert (M.literal_status solver lf2 = M.LTRUE); |

844 |
mkExclClause deferral f2 acc |

845 |
| AndF -> |

846 |
(* if the true f is a conjuction, then both conjunctions must be true *) |

847 |
let f1 = lfGetDest1 sort f in |

848 |
let lf1 = fhtMustFind fht f1 in |

849 |
assert (M.literal_status solver lf1 = M.LTRUE); |

850 |
let acc1 = mkExclClause deferral f1 acc in |

851 |
let f2 = lfGetDest2 sort f in |

852 |
let lf2 = fhtMustFind fht f2 in |

853 |
assert (M.literal_status solver lf2 = M.LTRUE); |

854 |
mkExclClause deferral f2 acc1 |

855 |
| MuF |

856 |
| NuF -> |

857 |
let f1 = lfGetDest1 sort f in |

858 |
mkExclClause deferral f1 acc |

859 |
| _ -> |

860 |
(* if f is a trivial formula or modality, then add it ... *) |

861 |
(* ... to newbs *) |

862 |
bsetAdd newbs f; |

863 |
let defercandidate = lfGetDeferral sort f in |

864 |
(if (defercandidate != (Hashtbl.hash "ε") && |

865 |
(refocusing || deferral = defercandidate)) then |

866 |
bsetAdd newdefer f); |

867 |
(* ... and to the new clause *) |

868 |
(M.neg_lit (fhtMustFind fht f))::acc |

869 |
in |

870 |
let init_clause f acc = |

871 |
let deferral = |

872 |
if bsetMem deferralS f then ( |

873 |
lfGetDeferral sort f) |

874 |
else |

875 |
(Hashtbl.hash "ε") |

876 |
in |

877 |
mkExclClause deferral f acc |

878 |
in |

879 |
let clause = bsetFold init_clause bs [] in |

880 |
let okay = M.add_clause solver clause in |

881 |
assert (okay); |

882 |
Some (sort, newbs, newdefer) |

883 | |

884 |
let newState sort bs defer = |

885 |
let (func, sl) = !sortTable.(sort) in |

886 |
let producer = CoAlgLogics.getExpandingFunctionProducer func in |

887 |
let exp = producer sort bs defer sl in |

888 |
stateMake sort bs defer exp |

889 | |

890 |
let insertState parent sort bs defer = |

891 |
let child = |

892 |
match graphFindState sort (bs, defer) with |

893 |
| None -> |

894 |
let s = newState sort bs defer in |

895 |
graphInsertState sort (bs, defer) s; |

896 |
queueInsertState s; |

897 |
s |

898 |
| Some s -> s |

899 |
in |

900 |
coreAddChild parent child; |

901 |
stateAddParent child parent |

902 | |

903 |
let expandCore core = |

904 |
match getNextState core with |

905 |
| Some (sort, bs, defer) -> |

906 |
insertState core sort bs defer; |

907 |
queueInsertCore core |

908 |
| None -> |

909 |
let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in |

910 |
if isUnsat then propagateUnsat [UCore (core, false)] |

911 |
else coreSetStatus core Open |

912 | |

913 | |

914 |
let insertCore sort bs defer = |

915 |
match graphFindCore sort (bs, defer) with |

916 |
| None -> |

917 |
let c = newCore sort bs defer in |

918 |
graphInsertCore sort (bs, defer) c; |

919 |
queueInsertCore c; |

920 |
c |

921 |
| Some c -> c |

922 | |

923 |
let insertRule state dep chldrn = |

924 |
let chldrn = listFromLazylist chldrn in |

925 |
let insert (isUns, acc) (sort, bs, defer) = |

926 |
let bs1 = bsetAddTBox sort bs in |

927 |
let core = insertCore sort bs1 defer in |

928 |
let isUns1 = if coreGetStatus core = Unsat then isUns else false in |

929 |
(isUns1, core::acc) |

930 |
in |

931 |
let (isUnsat, children) = List.fold_left insert (true, []) chldrn in |

932 |
let idx = stateAddRule state dep (List.rev children) in |

933 |
List.iter (fun c -> coreAddParent c state idx) children; |

934 |
if isUnsat then begin |

935 |
propagateUnsat [UState (state, Some idx)]; |

936 |
false |

937 |
end else true |

938 | |

939 |
let rec insertAllRules state = function |

940 |
| [] -> true |

941 |
| (dep, chldrn)::tl -> |

942 |
let notUnsat = insertRule state dep chldrn in |

943 |
if notUnsat then insertAllRules state tl else false |

944 | |

945 |
let expandState state = |

946 |
match stateNextRule state with |

947 |
| MultipleElements rules -> |

948 |
let notUnsat = insertAllRules state rules in |

949 |
if notUnsat then stateSetStatus state Open |

950 |
| SingleElement (dep, chldrn) -> |

951 |
let notUnsat = insertRule state dep chldrn in |

952 |
if notUnsat then queueInsertState state else () |

953 |
| NoMoreElements -> stateSetStatus state Open |

954 | |

955 | |

956 |
let expandCnstr cset = |

957 |
let nht = nhtInit () in |

958 |
let mkCores f = |

959 |
let (sort, lf) as nom = atFormulaGetNominal f in |

960 |
let nomset = |

961 |
match nhtFind nht nom with |

962 |
| Some ns -> ns |

963 |
| None -> |

964 |
let cset1 = csetCopy cset in |

965 |
csetRemDot cset1; |

966 |
let bs = csetAddTBox sort cset1 in |

967 |
bsetAdd bs lf; |

968 |
nhtAdd nht nom bs; |

969 |
bs |

970 |
in |

971 |
bsetAdd nomset (atFormulaGetSubformula f) |

972 |
in |

973 |
csetIter cset mkCores; |

974 |
let inCores (sort, _) bs (isUns, acc) = |

975 |
let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *) |

976 |
coreAddConstraintParent core cset; |

977 |
(coreGetStatus core = Unsat || isUns, core::acc) |

978 |
in |

979 |
let (isUnsat, children) = nhtFold inCores nht (false, []) in |

980 |
if isUnsat then propagateUnsat [UCnstr cset] |

981 |
else |

982 |
match graphFindCnstr cset with |

983 |
| Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents) |

984 |
| _ -> assert false |

985 | |

986 | |

987 |
(*****************************************************************************) |

988 |
(* The Main Loop *) |

989 |
(*****************************************************************************) |

990 | |

991 |
let expandNodesLoop (recursiveAction: unit -> unit) = |

992 |
match queueGetElement () with |

993 |
| QState state -> |

994 |
if stateGetStatus state = Expandable then begin |

995 |
expandState state; |

996 |
if doNominalPropagation () then begin |

997 |
propagateNominals (); |

998 |
if doSatPropagation () then propagateUnsatMu () |

999 |
end else () |

1000 |
end else (); |

1001 |
recursiveAction () |

1002 |
| QCore core -> |

1003 |
if coreGetStatus core = Expandable then begin |

1004 |
expandCore core; |

1005 |
if doNominalPropagation () then begin |

1006 |
propagateNominals (); |

1007 |
if doSatPropagation () then propagateUnsatMu () |

1008 |
end else () |

1009 |
end else (); |

1010 |
recursiveAction () |

1011 |
| QCnstr cset -> |

1012 |
expandCnstr cset; |

1013 |
recursiveAction () |

1014 |
| QEmpty -> () |

1015 | |

1016 |
let runReasonerStep () = |

1017 |
let void () = () in |

1018 |
expandNodesLoop void; (* expand at most one node *) |

1019 |
(* if this emptied the queue *) |

1020 |
if queueIsEmpty () then begin |

1021 |
(* then check whether the nominals would add further queue elements *) |

1022 |
print_endline "Propagating nominals..."; |

1023 |
propagateNominals () |

1024 |
end else () (* else: the next step would be to expand another node *) |

1025 | |

1026 |
let rec buildGraphLoop () = |

1027 |
let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in |

1028 |
expandNodesFurther (); (* expand as many queue elements as possible *) |

1029 |
propagateNominals (); |

1030 |
(* if propagating nominals added some more queue members, do all again.. *) |

1031 |
if queueIsEmpty () then () else buildGraphLoop () |

1032 | |

1033 |
let initReasoner sorts nomTable tbox sf = |

1034 |
sortTable := Array.copy sorts; |

1035 |
let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in |

1036 |
let sort = fst sf in |

1037 |
let bs1 = bsetAddTBox sort bs in |

1038 |
let deferrals = bsetMakeRealEmpty() in |

1039 |
let markDeferral f = |

1040 |
if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then ( |

1041 |
bsetAdd deferrals f;) |

1042 |
in |

1043 |
bsetIter markDeferral bs; |

1044 |
graphInit (); |

1045 |
queueInit (); |

1046 |
let root = insertCore sort bs1 deferrals in |

1047 |
graphAddRoot root |

1048 | |

1049 |
let isRootSat () = |

1050 |
match coreGetStatus (graphGetRoot ()) with |

1051 |
| Expandable -> None |

1052 |
| Unsat -> Some false |

1053 |
| Sat -> Some true |

1054 |
| Open -> if (queueIsEmpty()) then Some true else None |

1055 | |

1056 |
let reasonerFinished () = |

1057 |
match coreGetStatus (graphGetRoot ()) with |

1058 |
| Expandable -> false |

1059 |
| Unsat |

1060 |
| Sat -> true |

1061 |
| Open -> queueIsEmpty () |

1062 | |

1063 | |

1064 |
(** A graph-tableau-based decision procedure framework for coalgebraic logics. |

1065 |
@param verbose An optional switch which determines |

1066 |
whether the procedure shall print some information on the standard output. |

1067 |
The default is false. |

1068 |
@param sorts An array mapping each sort (represented as an integer) |

1069 |
to a functor and a list of sorts which are the arguments of the functor. |

1070 |
@param nomTable A partial function mapping nominals (represented as strings) |

1071 |
to their sorts. |

1072 |
@param tbox A list of sorted formulae. |

1073 |
@param sf A sorted formula. |

1074 |
@return True if sf is satisfiable wrt tbox, false otherwise. |

1075 |
*) |

1076 | |

1077 |
let isSat ?(verbose = false) sorts nomTable tbox sf = |

1078 |
let start = if verbose then Unix.gettimeofday () else 0. in |

1079 |
initReasoner sorts nomTable tbox sf; |

1080 |
let sat = |

1081 |
try |

1082 |
buildGraphLoop (); |

1083 |
propagateUnsatMu (); |

1084 |
(* get whether the root is satisfiable *) |

1085 |
(* we know that the reasoner finished, so the value is there, *) |

1086 |
(* i.e. isRootSat() will give a "Some x" and not "None" *) |

1087 |
CU.fromSome (isRootSat()) |

1088 |
with CoAlg_finished res -> res |

1089 |
in |

1090 |
(* print some statistics *) |

1091 |
if verbose then |

1092 |
let stop = Unix.gettimeofday () in |

1093 |
let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in |

1094 |
print_newline (); |

1095 |
print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf)); |

1096 |
let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in |

1097 |
print_endline ("Added Size: " ^ (string_of_int size)); |

1098 |
(* |

1099 |
print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1)); |

1100 |
let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in |

1101 |
print_endline ("Added Size: " ^ (string_of_int nsize)); |

1102 |
*) |

1103 |
print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); |

1104 |
print_endline ("Time: " ^ (string_of_float (stop -. start))); |

1105 |
print_endline ("Generated states: " ^ (string_of_int (graphSizeState ()))); |

1106 |
print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ()))); |

1107 |
print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ()))); |

1108 |
print_newline () |

1109 |
else (); |

1110 |
sat |