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

History | View | Annotate | Download (33.3 KB)

1 | 4fd28192 | Thorsten Wißmann | (** 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 | c2cc0c2e | Thorsten Wißmann | module CU = CoolUtils |

11 | |||

12 | 4fd28192 | Thorsten Wißmann | type sortTable = CoAlgMisc.sortTable |

13 | |||

14 | c78c1ce0 | Thorsten Wißmann | type nomTable = string -> CoAlgFormula.sort option |

15 | |||

16 | type assumptions = CoAlgFormula.sortedFormula list |
||

17 | |||

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

19 | |||

20 | f335015f | Thorsten Wißmann | exception ReasonerError of string |

21 | 4fd28192 | Thorsten Wißmann | |

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 | 6d64bc5a | Christoph Egger | | None -> raise (ReasonerError "?") |

31 | | Some SatC -> true |
||

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

33 | | Some (UnexpandedC _) |
||

34 | | Some UnsatC -> false |
||

35 | |||

36 | 4fd28192 | Thorsten Wißmann | |

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 | 6bbde09c | Christoph Egger | let propagateSatMu () = |

117 | let setFinishingStates = setEmptyState () in |
||

118 | let setFinishingCores = setEmptyCore () in |
||

119 | let setStates = setEmptyState () in |
||

120 | let setCores = setEmptyCore () in |
||

121 | 07a36b24 | Christoph Egger | let setSatStates = setEmptyState () in |

122 | let setSatCores = setEmptyCore () in |
||

123 | 6bbde09c | Christoph Egger | let emptySet = bsetMakeRealEmpty () in |

124 | |||

125 | let stateCollector state = |
||

126 | match stateGetStatus state with |
||

127 | 07a36b24 | Christoph Egger | | Unsat -> () |

128 | | Sat -> |
||

129 | setAddState setSatStates state |
||

130 | 6bbde09c | Christoph Egger | | Expandable |

131 | | Open -> |
||

132 | 46cd6856 | Christoph Egger | if stateGetStatus state == Open && List.length (stateGetRules state) == 0 |

133 | 6bbde09c | Christoph Egger | then begin |

134 | 46cd6856 | Christoph Egger | setAddState setSatStates state; |

135 | stateSetStatus state Sat |
||

136 | end else begin |
||

137 | setAddState setStates state; |
||

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

139 | then begin |
||

140 | 6bbde09c | Christoph Egger | print_endline (stateToString state); |

141 | setAddState setFinishingStates state |
||

142 | end |
||

143 | 46cd6856 | Christoph Egger | else () |

144 | end |
||

145 | 6bbde09c | Christoph Egger | in |

146 | let coreCollector core = |
||

147 | match coreGetStatus core with |
||

148 | 07a36b24 | Christoph Egger | | Unsat -> () |

149 | | Sat -> |
||

150 | setAddCore setSatCores core |
||

151 | 6bbde09c | Christoph Egger | | Expandable |

152 | | Open -> |
||

153 | setAddCore setCores core; |
||

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

155 | then begin |
||

156 | print_endline (coreToString core); |
||

157 | setAddCore setFinishingCores core |
||

158 | end |
||

159 | else () |
||

160 | in |
||

161 | graphIterStates stateCollector; |
||

162 | graphIterCores coreCollector; |
||

163 | |||

164 | (* |
||

165 | In a fixpoint the set called setStates / setCores is narrowed down. |
||

166 | |||

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

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

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

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

171 | |||

172 | Only those finishing nodes are retained that have allowed or |
||

173 | Successfull Children. |
||

174 | *) |
||

175 | |||

176 | let rec fixpointstep setStates setCores = |
||

177 | 67b07e54 | Christoph Egger | let allowedStates = setEmptyState () in |

178 | let allowedCores = setEmptyCore () in |
||

179 | 6bbde09c | Christoph Egger | |

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

181 | 2fba43c0 | Christoph Egger | if not (setMemCore setCores core || setMemCore setSatCores core) then () |

182 | 67b07e54 | Christoph Egger | else begin |

183 | 6bbde09c | Christoph Egger | let children = coreGetChildren core in |

184 | 67b07e54 | Christoph Egger | let acceptable = |

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

186 | children |
||

187 | in |
||

188 | 6bbde09c | Christoph Egger | if acceptable then begin |

189 | print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed"); |
||

190 | setAddCore allowedCores core; |
||

191 | List.iter (fun (state, _) -> visitParentCores state) |
||

192 | (coreGetParents core) |
||

193 | end |
||

194 | end |
||

195 | |||

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

197 | 2fba43c0 | Christoph Egger | if not (setMemState setStates state || setMemState setSatStates state) then () |

198 | 67b07e54 | Christoph Egger | else begin |

199 | 6bbde09c | Christoph Egger | let rules = stateGetRules state in |

200 | let ruleiter (dependencies, corelist) = |
||

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

202 | corelist |
||

203 | 6bbde09c | Christoph Egger | in |

204 | let acceptable = List.for_all ruleiter rules in |
||

205 | if acceptable then begin |
||

206 | print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed"); |
||

207 | setAddState allowedStates state; |
||

208 | 67b07e54 | Christoph Egger | List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core) |

209 | 6bbde09c | Christoph Egger | (stateGetParents state) |

210 | end |
||

211 | end |
||

212 | in |
||

213 | |||

214 | 07a36b24 | Christoph Egger | (* All rule applications need to still be potentially Sat for a |

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

216 | *) |
||

217 | let checkFinishingState (state : state) = |
||

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

219 | 0a6a3df5 | Christoph Egger | List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist |

220 | 07a36b24 | Christoph Egger | in |

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

222 | setAddState allowedStates state; |
||

223 | visitParentCores state |
||

224 | end |
||

225 | |||

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

227 | * to be considered for the fixpoint |
||

228 | *) |
||

229 | and checkFinishingCore (core : core) = |
||

230 | 0a6a3df5 | Christoph Egger | if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state)) |

231 | 07a36b24 | Christoph Egger | (coreGetChildren core)) |

232 | then begin |
||

233 | setAddCore allowedCores core; |
||

234 | visitParentStates core |
||

235 | end |
||

236 | in |
||

237 | setIterState checkFinishingState setFinishingStates; |
||

238 | setIterCore checkFinishingCore setFinishingCores; |
||

239 | setIterState visitParentCores setSatStates; |
||

240 | setIterCore visitParentStates setSatCores; |
||

241 | |||

242 | 6bbde09c | Christoph Egger | |

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

244 | 07a36b24 | Christoph Egger | (setLengthCore setCores) = (setLengthCore allowedCores) |

245 | 6bbde09c | Christoph Egger | then begin |

246 | 07a36b24 | Christoph Egger | setIterState (fun state -> stateSetStatus state Sat) setStates; |

247 | setIterCore (fun core -> coreSetStatus core Sat) setCores; |
||

248 | end else |
||

249 | 6bbde09c | Christoph Egger | fixpointstep allowedStates allowedCores |

250 | in |
||

251 | fixpointstep setStates setCores |
||

252 | |||

253 | |||

254 | 4fd28192 | Thorsten Wißmann | (*****************************************************************************) |

255 | (* Propagation of Unsatisfiability *) |
||

256 | (*****************************************************************************) |
||

257 | |||

258 | let isConstraintUnsat cset = |
||

259 | match graphFindCnstr cset with |
||

260 | | None -> assert false |
||

261 | | Some UnsatC -> true |
||

262 | | _ -> false |
||

263 | |||

264 | 433c8a2e | Thorsten Wißmann | let fhtMustFind fht f = |

265 | 4fd28192 | Thorsten Wißmann | match fhtFind fht f with |

266 | | Some l -> l |
||

267 | | None -> assert false |
||

268 | |||

269 | 433c8a2e | Thorsten Wißmann | let lhtMustFind lht l = |

270 | match lhtFind lht l with |
||

271 | 4fd28192 | Thorsten Wißmann | | Some f -> f |

272 | | None -> assert false |
||

273 | 01bf25db | Thorsten Wißmann | |

274 | 7b21fbae | Christoph Egger | |

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

276 | information backwards *) |
||

277 | 433c8a2e | Thorsten Wißmann | let rec propagateUnsat = function |

278 | 4fd28192 | Thorsten Wißmann | | [] -> () |

279 | | propElem::tl -> |
||

280 | let tl1 = |
||

281 | match propElem with |
||

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

283 | match stateGetStatus state with |
||

284 | | Unsat -> tl |
||

285 | 73762b19 | Thorsten Wißmann | | Sat -> raise (ReasonerError ("Propagation tells state " |

286 | ^(string_of_int (stateGetIdx state)) |
||

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

288 | 4fd28192 | Thorsten Wißmann | | Open |

289 | | Expandable -> |
||

290 | let mbs = |
||

291 | match idxopt with |
||

292 | | None -> stateGetBs state |
||

293 | | Some idx -> |
||

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

295 | let getBs core = |
||

296 | assert (coreGetStatus core = Unsat); |
||

297 | coreGetBs core |
||

298 | in |
||

299 | dep (List.map getBs children) |
||

300 | in |
||

301 | stateSetBs state mbs; |
||

302 | stateSetStatus state Unsat; |
||

303 | let prop acc core = |
||

304 | let turnsUnsat = |
||

305 | match coreGetStatus core with |
||

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

307 | | Expandable |
||

308 | | Unsat |
||

309 | | Sat -> false |
||

310 | in |
||

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

312 | in |
||

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

314 | end |
||

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

316 | match coreGetStatus core with |
||

317 | | Unsat -> tl |
||

318 | 73762b19 | Thorsten Wißmann | | Sat -> raise (ReasonerError ("Propagation tells core " |

319 | ^(string_of_int (coreGetIdx core)) |
||

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

321 | 4fd28192 | Thorsten Wißmann | | Open |

322 | | Expandable -> |
||

323 | let mbs = |
||

324 | if comesFromCnstr then coreGetBs core |
||

325 | else |
||

326 | let bs = coreGetBs core in |
||

327 | let solver = coreGetSolver core in |
||

328 | let fht = coreGetFht core in |
||

329 | let lht = lhtInit () in |
||

330 | let addLits f acc = |
||

331 | let lit = fhtMustFind fht f in |
||

332 | lhtAdd lht lit f; |
||

333 | lit::acc |
||

334 | in |
||

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

336 | let addClauses state = |
||

337 | let cbs = stateGetBs state in |
||

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

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

340 | assert okay |
||

341 | in |
||

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

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

344 | assert (not isSat); |
||

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

346 | let confls = M.get_conflict solver in |
||

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

348 | res |
||

349 | in |
||

350 | coreSetBs core mbs; |
||

351 | coreSetStatus core Unsat; |
||

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

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

354 | let turnsUnsat = |
||

355 | match stateGetStatus state with |
||

356 | | Open |
||

357 | | Expandable -> |
||

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

359 | | Unsat |
||

360 | | Sat -> false |
||

361 | in |
||

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

363 | in |
||

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

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

366 | end |
||

367 | | UCnstr cset -> |
||

368 | match graphFindCnstr cset with |
||

369 | | None |
||

370 | | Some SatC -> assert false |
||

371 | | Some UnsatC -> tl |
||

372 | | Some (UnexpandedC nodes) |
||

373 | | Some (OpenC nodes) -> |
||

374 | graphReplaceCnstr cset UnsatC; |
||

375 | let prop acc node = |
||

376 | match node with |
||

377 | | State state -> |
||

378 | 3eb8fabd | Christoph Egger | let turnsUnsat = |

379 | 4fd28192 | Thorsten Wißmann | match stateGetStatus state with |

380 | | Expandable |
||

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

382 | | Unsat |
||

383 | | Sat -> false |
||

384 | in |
||

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

386 | | Core core -> |
||

387 | let turnsUnsat = |
||

388 | match coreGetStatus core with |
||

389 | | Expandable |
||

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

391 | | Unsat |
||

392 | | Sat -> false |
||

393 | in |
||

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

395 | in |
||

396 | List.fold_left prop tl nodes |
||

397 | in |
||

398 | propagateUnsat tl1 |
||

399 | |||

400 | |||

401 | (*****************************************************************************) |
||

402 | (* Propagation of Nominal Constraints *) |
||

403 | (*****************************************************************************) |
||

404 | |||

405 | 433c8a2e | Thorsten Wißmann | let extractAts sort bs = |

406 | 4fd28192 | Thorsten Wißmann | let ats = csetMake () in |

407 | let procNom nom f = |
||

408 | match lfGetType sort f with |
||

409 | | AndF |
||

410 | | OrF -> () |
||

411 | 3b055ae8 | dirk | | TrueFalseF |

412 | 4fd28192 | Thorsten Wißmann | | AtF -> () |

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

414 | in |
||

415 | let getAts f = |
||

416 | match lfGetType sort f with |
||

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

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

419 | | _ -> () |
||

420 | in |
||

421 | bsetIter getAts bs; |
||

422 | ats |
||

423 | |||

424 | 433c8a2e | Thorsten Wißmann | let detConstraintsState state = |

425 | 4fd28192 | Thorsten Wißmann | let procRule accR (_, chldrn) = |

426 | let procChldrn accC core = |
||

427 | if coreGetStatus core = Unsat then accC |
||

428 | else cssUnion accC (coreGetConstraints core) |
||

429 | in |
||

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

431 | let procOrset csetO accO = |
||

432 | let mkUnion csetU accU = |
||

433 | let cset = csetUnion csetO csetU in |
||

434 | cssAdd cset accU |
||

435 | in |
||

436 | cssFold mkUnion accR accO |
||

437 | in |
||

438 | cssFold procOrset orset cssEmpty |
||

439 | in |
||

440 | let sort = stateGetSort state in |
||

441 | let bs = stateGetBs state in |
||

442 | let ats = extractAts sort bs in |
||

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

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

445 | |||

446 | 433c8a2e | Thorsten Wißmann | let detConstraintsCore core = |

447 | 4fd28192 | Thorsten Wißmann | let sort = coreGetSort core in |

448 | let bs = coreGetBs core in |
||

449 | let ats = extractAts sort bs in |
||

450 | let addCnstr acc state = |
||

451 | if stateGetStatus state = Unsat then acc |
||

452 | else |
||

453 | let csets = stateGetConstraints state in |
||

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

455 | cssUnion csets acc |
||

456 | in |
||

457 | let initInner = |
||

458 | if coreGetStatus core = Expandable then |
||

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

460 | let cset = ats in |
||

461 | csetAddDot cset; |
||

462 | cssSingleton cset |
||

463 | else cssEmpty |
||

464 | in |
||

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

466 | |||

467 | 433c8a2e | Thorsten Wißmann | let rec propNom = function |

468 | 4fd28192 | Thorsten Wißmann | | [] -> () |

469 | | node::tl -> |
||

470 | let tl1 = |
||

471 | match node with |
||

472 | | State state -> |
||

473 | if stateGetStatus state = Unsat then tl |
||

474 | else |
||

475 | let csets = detConstraintsState state in |
||

476 | let oldcsets = stateGetConstraints state in |
||

477 | if cssEqual csets oldcsets then tl |
||

478 | else begin |
||

479 | stateSetConstraints state csets; |
||

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

481 | end |
||

482 | | Core core -> |
||

483 | if coreGetStatus core = Unsat then tl |
||

484 | else |
||

485 | let csets = detConstraintsCore core in |
||

486 | let oldcsets = coreGetConstraints core in |
||

487 | if cssEqual csets oldcsets then tl |
||

488 | else begin |
||

489 | coreSetConstraints core csets; |
||

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

491 | end |
||

492 | in |
||

493 | propNom tl1 |
||

494 | |||

495 | let updateConstraints node elemU csets = |
||

496 | let update cset acc = |
||

497 | let cnstr = |
||

498 | match graphFindCnstr cset with |
||

499 | | Some cn -> cn |
||

500 | | None -> |
||

501 | let cn = UnexpandedC [] in |
||

502 | graphInsertCnstr cset cn; |
||

503 | queueInsertCnstr cset; |
||

504 | cn |
||

505 | in |
||

506 | match cnstr with |
||

507 | | UnsatC -> acc |
||

508 | | UnexpandedC parents -> |
||

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

510 | false |
||

511 | | OpenC parents -> |
||

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

513 | false |
||

514 | | SatC -> false |
||

515 | in |
||

516 | let isUnsat = cssFold update csets true in |
||

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

518 | |||

519 | 433c8a2e | Thorsten Wißmann | let propagateNominals () = |

520 | 4fd28192 | Thorsten Wißmann | let init = cssSingleton (csetMake ()) in |

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

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

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

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

525 | graphClearCnstr (); |
||

526 | let fktS state = |
||

527 | if stateGetStatus state = Unsat then () |
||

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

529 | in |
||

530 | graphIterStates fktS; |
||

531 | let fktC core = |
||

532 | if coreGetStatus core = Unsat then () |
||

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

534 | in |
||

535 | graphIterCores fktC |
||

536 | |||

537 | |||

538 | (*****************************************************************************) |
||

539 | (* Node Expansions *) |
||

540 | (*****************************************************************************) |
||

541 | |||

542 | 433c8a2e | Thorsten Wißmann | let getLit sort fht solver f = |

543 | 4fd28192 | Thorsten Wißmann | match fhtFind fht f with |

544 | | Some lit -> lit |
||

545 | | None -> |
||

546 | let var = M.new_variable solver in |
||

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

548 | fhtAdd fht f lit; |
||

549 | let () = |
||

550 | match lfGetNeg sort f with |
||

551 | | None -> () |
||

552 | | Some nf -> |
||

553 | let nlit = M.neg_lit lit in |
||

554 | fhtAdd fht nf nlit; |
||

555 | in |
||

556 | lit |
||

557 | |||

558 | 16af388e | Christoph Egger | let newCore sort bs defer = |

559 | e0f19999 | Thorsten Wißmann | (* when creating a now core from a set of formulas bs |

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

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

562 | Then we do this by: |
||

563 | |||

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

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

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

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

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

569 | subformulas by a clause: |
||

570 | *) |
||

571 | 4fd28192 | Thorsten Wißmann | let fht = fhtInit () in |

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

573 | 433c8a2e | Thorsten Wißmann | let rec addClauses f = |

574 | e0f19999 | Thorsten Wißmann | (* step 1: create a literal in the satsolver representing the formula f *) |

575 | 433c8a2e | Thorsten Wißmann | let lf = getLit sort fht solver f in |

576 | e0f19999 | Thorsten Wißmann | (* step 2: encode relation to possible subformulas *) |

577 | 4fd28192 | Thorsten Wißmann | match lfGetType sort f with |

578 | | OrF -> |
||

579 | e0f19999 | Thorsten Wißmann | (* |

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

581 | fill fht such that it says: |
||

582 | |||

583 | f |---> lf |
||

584 | f1 |---> lf1 |
||

585 | f2 |---> lf2 |
||

586 | *) |
||

587 | 4fd28192 | Thorsten Wißmann | let f1 = lfGetDest1 sort f in |

588 | let f2 = lfGetDest2 sort f in |
||

589 | addClauses f1; |
||

590 | addClauses f2; |
||

591 | let lf1 = fhtMustFind fht f1 in |
||

592 | let lf2 = fhtMustFind fht f2 in |
||

593 | e0f19999 | Thorsten Wißmann | (* |

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

595 | *) |
||

596 | 4fd28192 | Thorsten Wißmann | let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in |

597 | assert (okay) |
||

598 | | AndF -> |
||

599 | e0f19999 | Thorsten Wißmann | (* |

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

601 | fill fht such that it says: |
||

602 | |||

603 | f |---> lf |
||

604 | f1 |---> lf1 |
||

605 | f2 |---> lf2 |
||

606 | *) |
||

607 | 4fd28192 | Thorsten Wißmann | let f1 = lfGetDest1 sort f in |

608 | let f2 = lfGetDest2 sort f in |
||

609 | addClauses f1; |
||

610 | addClauses f2; |
||

611 | let lf1 = fhtMustFind fht f1 in |
||

612 | let lf2 = fhtMustFind fht f2 in |
||

613 | e0f19999 | Thorsten Wißmann | (* |

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

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

616 | *) |
||

617 | 4fd28192 | Thorsten Wißmann | let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in |

618 | assert (okay1); |
||

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

620 | assert (okay2) |
||

621 | 3eb8fabd | Christoph Egger | | MuF |

622 | | NuF -> |
||

623 | (* |
||

624 | 9b6bdd74 | Christoph Egger | Dest of a fixpoint is it's unfolded version. This adds just |

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

626 | though not without nontrivial transformation of code |
||

627 | |||

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

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

630 | |||

631 | Then adding lf -> lf1 to minisat |
||

632 | 3eb8fabd | Christoph Egger | *) |

633 | let f1 = lfGetDest1 sort f in |
||

634 | addClauses f1; |
||

635 | let lf1 = fhtMustFind fht f1 in |
||

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

637 | 9b6bdd74 | Christoph Egger | assert (okay1); |

638 | 4fd28192 | Thorsten Wißmann | | _ -> () |

639 | e0f19999 | Thorsten Wißmann | (* case 2.(c) |

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

641 | *) |
||

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

643 | bsetIter addClauses bs; |
||

644 | 16af388e | Christoph Egger | coreMake sort bs defer solver fht |

645 | 4fd28192 | Thorsten Wißmann | |

646 | 433c8a2e | Thorsten Wißmann | let getNextState core = |

647 | e0f19999 | Thorsten Wißmann | (* Create a new state, which is obtained by a satisfying assignment of the |

648 | literals of the minisat solver. |
||

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

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

651 | minisat calls. |
||

652 | *) |
||

653 | 4fd28192 | Thorsten Wißmann | let bs = coreGetBs core in |

654 | 16af388e | Christoph Egger | let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in |

655 | let deferralS = |
||

656 | if refocusing then |
||

657 | bsetCopy bs |
||

658 | else |
||

659 | coreGetDeferral core |
||

660 | in |
||

661 | 4fd28192 | Thorsten Wißmann | let fht = coreGetFht core in |

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

663 | let solver = coreGetSolver core in |
||

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

665 | e0f19999 | Thorsten Wißmann | (* Clearly, if the current core is unsatisfiable, no further child state can |

666 | be created *) |
||

667 | 4fd28192 | Thorsten Wißmann | if not isSat then None |

668 | else |
||

669 | let sort = coreGetSort core in |
||

670 | e0f19999 | Thorsten Wißmann | (* create a new set of formulas newbs with the property: |

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

672 | satisfiable. |
||

673 | *) |
||

674 | 4fd28192 | Thorsten Wißmann | let newbs = bsetMake () in |

675 | 16af388e | Christoph Egger | let newdefer = bsetMakeRealEmpty () in |

676 | e0f19999 | Thorsten Wißmann | (* if newbs = { l_1, .... l_n }, i.e. |

677 | |||

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

679 | |||

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

681 | adding another clause |
||

682 | |||

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

684 | |||

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

686 | *) |
||

687 | b395c870 | Christoph Egger | let rec mkExclClause deferral f acc = |

688 | e0f19999 | Thorsten Wißmann | (* f is a formula that is true in the current satisfying assignment *) |

689 | 4fd28192 | Thorsten Wißmann | match lfGetType sort f with |

690 | 433c8a2e | Thorsten Wißmann | | OrF -> |

691 | e0f19999 | Thorsten Wißmann | (* if f is true and a disjunction, then one of its disjuncts is true *) |

692 | 4fd28192 | Thorsten Wißmann | let f1 = lfGetDest1 sort f in |

693 | 433c8a2e | Thorsten Wißmann | let lf1 = fhtMustFind fht f1 in |

694 | e0f19999 | Thorsten Wißmann | (* if the first disjunct f1 is true, then we need to add subformulas |

695 | of f1 to newbs&clause *) |
||

696 | b395c870 | Christoph Egger | if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc |

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

698 | e0f19999 | Thorsten Wißmann | (* otherwise f2 must be true *) |

699 | 4fd28192 | Thorsten Wißmann | let f2 = lfGetDest2 sort f in |

700 | let lf2 = fhtMustFind fht f2 in |
||

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

702 | b395c870 | Christoph Egger | mkExclClause deferral f2 acc |

703 | 4fd28192 | Thorsten Wißmann | | AndF -> |

704 | e0f19999 | Thorsten Wißmann | (* if the true f is a conjuction, then both conjunctions must be true *) |

705 | 4fd28192 | Thorsten Wißmann | let f1 = lfGetDest1 sort f in |

706 | let lf1 = fhtMustFind fht f1 in |
||

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

708 | b395c870 | Christoph Egger | let acc1 = mkExclClause deferral f1 acc in |

709 | 4fd28192 | Thorsten Wißmann | let f2 = lfGetDest2 sort f in |

710 | let lf2 = fhtMustFind fht f2 in |
||

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

712 | b395c870 | Christoph Egger | mkExclClause deferral f2 acc1 |

713 | 3eb8fabd | Christoph Egger | | MuF |

714 | | NuF -> |
||

715 | let f1 = lfGetDest1 sort f in |
||

716 | b395c870 | Christoph Egger | mkExclClause deferral f1 acc |

717 | 4fd28192 | Thorsten Wißmann | | _ -> |

718 | b395c870 | Christoph Egger | (* if f is a trivial formula or modality, then add it ... *) |

719 | (* ... to newbs *) |
||

720 | bsetAdd newbs f; |
||

721 | let defercandidate = lfGetDeferral sort f in |
||

722 | 16af388e | Christoph Egger | (if (defercandidate != (Hashtbl.hash "ε") && |

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

724 | b395c870 | Christoph Egger | bsetAdd newdefer f); |

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

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

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

728 | b395c870 | Christoph Egger | let init_clause f acc = |

729 | let deferral = |
||

730 | 16af388e | Christoph Egger | if bsetMem deferralS f then ( |

731 | lfGetDeferral sort f) |
||

732 | b395c870 | Christoph Egger | else |

733 | (Hashtbl.hash "ε") |
||

734 | in |
||

735 | mkExclClause deferral f acc |
||

736 | in |
||

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

738 | 433c8a2e | Thorsten Wißmann | let okay = M.add_clause solver clause in |

739 | 4fd28192 | Thorsten Wißmann | assert (okay); |

740 | b395c870 | Christoph Egger | Some (sort, newbs, newdefer) |

741 | 4fd28192 | Thorsten Wißmann | |

742 | b395c870 | Christoph Egger | let newState sort bs defer = |

743 | 4fd28192 | Thorsten Wißmann | let (func, sl) = !sortTable.(sort) in |

744 | let producer = CoAlgLogics.getExpandingFunctionProducer func in |
||

745 | 16af388e | Christoph Egger | let exp = producer sort bs defer sl in |

746 | b395c870 | Christoph Egger | stateMake sort bs defer exp |

747 | 4fd28192 | Thorsten Wißmann | |

748 | b395c870 | Christoph Egger | let insertState parent sort bs defer = |

749 | 4fd28192 | Thorsten Wißmann | let child = |

750 | 16af388e | Christoph Egger | match graphFindState sort (bs, defer) with |

751 | 4fd28192 | Thorsten Wißmann | | None -> |

752 | b395c870 | Christoph Egger | let s = newState sort bs defer in |

753 | 16af388e | Christoph Egger | graphInsertState sort (bs, defer) s; |

754 | 4fd28192 | Thorsten Wißmann | queueInsertState s; |

755 | s |
||

756 | | Some s -> s |
||

757 | in |
||

758 | coreAddChild parent child; |
||

759 | stateAddParent child parent |
||

760 | |||

761 | let expandCore core = |
||

762 | match getNextState core with |
||

763 | b395c870 | Christoph Egger | | Some (sort, bs, defer) -> |

764 | insertState core sort bs defer; |
||

765 | 4fd28192 | Thorsten Wißmann | queueInsertCore core |

766 | | None -> |
||

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

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

769 | else coreSetStatus core Open |
||

770 | |||

771 | |||

772 | 16af388e | Christoph Egger | let insertCore sort bs defer = |

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

774 | 4fd28192 | Thorsten Wißmann | | None -> |

775 | 16af388e | Christoph Egger | let c = newCore sort bs defer in |

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

777 | queueInsertCore c; |
||

778 | c |
||

779 | 4fd28192 | Thorsten Wißmann | | Some c -> c |

780 | |||

781 | 433c8a2e | Thorsten Wißmann | let insertRule state dep chldrn = |

782 | let chldrn = listFromLazylist chldrn in |
||

783 | 16af388e | Christoph Egger | let insert (isUns, acc) (sort, bs, defer) = |

784 | 4fd28192 | Thorsten Wißmann | let bs1 = bsetAddTBox sort bs in |

785 | 16af388e | Christoph Egger | let core = insertCore sort bs1 defer in |

786 | 433c8a2e | Thorsten Wißmann | let isUns1 = if coreGetStatus core = Unsat then isUns else false in |

787 | (isUns1, core::acc) |
||

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

789 | 433c8a2e | Thorsten Wißmann | let (isUnsat, children) = List.fold_left insert (true, []) chldrn in |

790 | 4fd28192 | Thorsten Wißmann | let idx = stateAddRule state dep (List.rev children) in |

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

792 | 433c8a2e | Thorsten Wißmann | if isUnsat then begin |

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

794 | false |
||

795 | end else true |
||

796 | |||

797 | let rec insertAllRules state = function |
||

798 | | [] -> true |
||

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

800 | let notUnsat = insertRule state dep chldrn in |
||

801 | if notUnsat then insertAllRules state tl else false |
||

802 | 4fd28192 | Thorsten Wißmann | |

803 | let expandState state = |
||

804 | 433c8a2e | Thorsten Wißmann | match stateNextRule state with |

805 | 69243f7f | Thorsten Wißmann | | MultipleElements rules -> |

806 | 433c8a2e | Thorsten Wißmann | let notUnsat = insertAllRules state rules in |

807 | if notUnsat then stateSetStatus state Open |
||

808 | 69243f7f | Thorsten Wißmann | | SingleElement (dep, chldrn) -> |

809 | 433c8a2e | Thorsten Wißmann | let notUnsat = insertRule state dep chldrn in |

810 | if notUnsat then queueInsertState state else () |
||

811 | 69243f7f | Thorsten Wißmann | | NoMoreElements -> stateSetStatus state Open |

812 | 4fd28192 | Thorsten Wißmann | |

813 | |||

814 | let expandCnstr cset = |
||

815 | let nht = nhtInit () in |
||

816 | let mkCores f = |
||

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

818 | let nomset = |
||

819 | match nhtFind nht nom with |
||

820 | | Some ns -> ns |
||

821 | | None -> |
||

822 | let cset1 = csetCopy cset in |
||

823 | csetRemDot cset1; |
||

824 | let bs = csetAddTBox sort cset1 in |
||

825 | bsetAdd bs lf; |
||

826 | nhtAdd nht nom bs; |
||

827 | bs |
||

828 | in |
||

829 | bsetAdd nomset (atFormulaGetSubformula f) |
||

830 | in |
||

831 | csetIter cset mkCores; |
||

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

833 | 16af388e | Christoph Egger | let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *) |

834 | 4fd28192 | Thorsten Wißmann | coreAddConstraintParent core cset; |

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

836 | in |
||

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

838 | if isUnsat then propagateUnsat [UCnstr cset] |
||

839 | else |
||

840 | match graphFindCnstr cset with |
||

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

842 | | _ -> assert false |
||

843 | |||

844 | |||

845 | (*****************************************************************************) |
||

846 | (* The Main Loop *) |
||

847 | (*****************************************************************************) |
||

848 | |||

849 | 2679ab63 | Thorsten Wißmann | let expandNodesLoop (recursiveAction: unit -> unit) = |

850 | 4fd28192 | Thorsten Wißmann | match queueGetElement () with |

851 | | QState state -> |
||

852 | if stateGetStatus state = Expandable then begin |
||

853 | expandState state; |
||

854 | if doNominalPropagation () then begin |
||

855 | propagateNominals (); |
||

856 | 1d5d9896 | Christoph Egger | if doSatPropagation () then propagateSatMu () |

857 | 4fd28192 | Thorsten Wißmann | end else () |

858 | end else (); |
||

859 | 2679ab63 | Thorsten Wißmann | recursiveAction () |

860 | 4fd28192 | Thorsten Wißmann | | QCore core -> |

861 | if coreGetStatus core = Expandable then begin |
||

862 | expandCore core; |
||

863 | if doNominalPropagation () then begin |
||

864 | propagateNominals (); |
||

865 | 1d5d9896 | Christoph Egger | if doSatPropagation () then propagateSatMu () |

866 | 4fd28192 | Thorsten Wißmann | end else () |

867 | end else (); |
||

868 | 2679ab63 | Thorsten Wißmann | recursiveAction () |

869 | 4fd28192 | Thorsten Wißmann | | QCnstr cset -> |

870 | expandCnstr cset; |
||

871 | 2679ab63 | Thorsten Wißmann | recursiveAction () |

872 | 4fd28192 | Thorsten Wißmann | | QEmpty -> () |

873 | |||

874 | c2cc0c2e | Thorsten Wißmann | let runReasonerStep () = |

875 | 2679ab63 | Thorsten Wißmann | let void () = () in |

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

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

878 | if queueIsEmpty () then begin |
||

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

880 | print_endline "Propagating nominals..."; |
||

881 | propagateNominals () |
||

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

883 | c2cc0c2e | Thorsten Wißmann | |

884 | let rec buildGraphLoop () = |
||

885 | 2679ab63 | Thorsten Wißmann | let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in |

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

887 | propagateNominals (); |
||

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

889 | 4fd28192 | Thorsten Wißmann | if queueIsEmpty () then () else buildGraphLoop () |

890 | c2cc0c2e | Thorsten Wißmann | |

891 | let initReasoner sorts nomTable tbox sf = |
||

892 | sortTable := Array.copy sorts; |
||

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

894 | let sort = fst sf in |
||

895 | let bs1 = bsetAddTBox sort bs in |
||

896 | 16af388e | Christoph Egger | let deferrals = bsetMakeRealEmpty() in |

897 | let markDeferral f = |
||

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

899 | bsetAdd deferrals f;) |
||

900 | in |
||

901 | bsetIter markDeferral bs; |
||

902 | c2cc0c2e | Thorsten Wißmann | graphInit (); |

903 | queueInit (); |
||

904 | 16af388e | Christoph Egger | let root = insertCore sort bs1 deferrals in |

905 | c2cc0c2e | Thorsten Wißmann | graphAddRoot root |

906 | |||

907 | let isRootSat () = |
||

908 | match coreGetStatus (graphGetRoot ()) with |
||

909 | | Expandable -> None |
||

910 | | Unsat -> Some false |
||

911 | | Sat |
||

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

913 | |||

914 | let reasonerFinished () = |
||

915 | match coreGetStatus (graphGetRoot ()) with |
||

916 | | Expandable -> false |
||

917 | | Unsat |
||

918 | | Sat -> true |
||

919 | | Open -> queueIsEmpty () |
||

920 | 3eb8fabd | Christoph Egger | |

921 | c2cc0c2e | Thorsten Wißmann | |

922 | 4fd28192 | Thorsten Wißmann | (** A graph-tableau-based decision procedure framework for coalgebraic logics. |

923 | @param verbose An optional switch which determines |
||

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

925 | The default is false. |
||

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

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

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

929 | to their sorts. |
||

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

931 | @param sf A sorted formula. |
||

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

933 | *) |
||

934 | c2cc0c2e | Thorsten Wißmann | |

935 | 4fd28192 | Thorsten Wißmann | let isSat ?(verbose = false) sorts nomTable tbox sf = |

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

937 | c2cc0c2e | Thorsten Wißmann | initReasoner sorts nomTable tbox sf; |

938 | 4fd28192 | Thorsten Wißmann | let sat = |

939 | try |
||

940 | buildGraphLoop (); |
||

941 | c2cc0c2e | Thorsten Wißmann | (* get whether the root is satisfiable *) |

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

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

944 | CU.fromSome (isRootSat()) |
||

945 | 4fd28192 | Thorsten Wißmann | with CoAlg_finished res -> res |

946 | in |
||

947 | c2cc0c2e | Thorsten Wißmann | (* print some statistics *) |

948 | 4fd28192 | Thorsten Wißmann | if verbose then |

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

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

951 | print_newline (); |
||

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

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

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

955 | c2cc0c2e | Thorsten Wißmann | (* |

956 | 4fd28192 | Thorsten Wißmann | print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1)); |

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

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

959 | c2cc0c2e | Thorsten Wißmann | *) |

960 | 4fd28192 | Thorsten Wißmann | print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); |

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

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

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

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

965 | print_newline () |
||

966 | else (); |
||

967 | sat |