Revision e765822b src/lib/CoAlgReasoner.ml
src/lib/CoAlgReasoner.ml  

1  1 
(** A graphtableaubased decision procedure framework for coalgebraic logics. 
2 
@author Florian Widmann 

2 
@author Florian Widmann, Daniel Hausmann


3  3 
*) 
4  4  
5  5 
open CoAlgMisc 
...  ...  
54  54 
(* Propagation of Satisfiability *) 
55  55 
(*****************************************************************************) 
56  56  
57 
let propSatFindSucc setCnstr cset = 

58 
if csetHasDot cset then false 

59 
else 

60 
match graphFindCnstr cset with 

61 
 None > raise (ReasonerError "?") 

62 
 Some SatC > true 

63 
 Some (OpenC _) > setMemCnstr setCnstr cset 

64 
 Some (UnexpandedC _) 

65 
 Some UnsatC > false 

66  
67  
68 
let rec propSat setStates setCores setCnstr = function 

69 
 [] > () 

70 
 propElem::tl > 

71 
let tl1 = 

72 
match propElem with 

73 
 UState (state, _) > 

74 
if setMemState setStates state then 

75 
let cnstrs = stateGetConstraints state in 

76 
let isStillOpen = cssExists (fun c > propSatFindSucc setCnstr c) cnstrs in 

77 
if isStillOpen then () else setRemoveState setStates state 

78 
else (); 

79 
tl 

80 
 UCore (core, _) > 

81 
if setMemCore setCores core then 

82 
let cnstrs = coreGetConstraints core in 

83 
let isStillOpen = cssExists (fun c > propSatFindSucc setCnstr c) cnstrs in 

84 
if isStillOpen then tl else begin 

85 
setRemoveCore setCores core; 

86 
let cnstrPar = coreGetConstraintParents core in 

87 
List.fold_left (fun acc cset > (UCnstr cset)::acc) tl cnstrPar 

88 
end 

89 
else tl 

90 
 UCnstr cset > 

91 
if setMemCnstr setCnstr cset then begin 

92 
setRemoveCnstr setCnstr cset; 

93 
match graphFindCnstr cset with 

94 
 Some (OpenC nodes) > 

95 
let prop acc node = 

96 
match node with 

97 
 Core core > (UCore (core, true))::acc 

98 
 State state > (UState (state, None))::acc 

99 
in 

100 
List.fold_left prop tl nodes 

101 
 _ > assert false 

102 
end else tl 

103 
in 

104 
propSat setStates setCores setCnstr tl1 

105  
106 
let propagateSat () = 

107 
let setStates = setEmptyState () in 

108 
let setCores = setEmptyCore () in 

109 
let setCnstr = setEmptyCnstr () in 

110 
let fktS1 state = 

111 
match stateGetStatus state with 

112 
 Expandable 

113 
 Open > setAddState setStates state 

114 
 Unsat 

115 
 Sat > () 

116 
in 

117 
graphIterStates fktS1; 

118 
let fktC1 core = 

119 
match coreGetStatus core with 

120 
 Expandable 

121 
 Open > setAddCore setCores core 

122 
 Unsat 

123 
 Sat > () 

124 
in 

125 
graphIterCores fktC1; 

126 
let cfkt1 cset cnstr = 

127 
if csetHasDot cset then () 

128 
else 

129 
match cnstr with 

130 
 OpenC _ > setAddCnstr setCnstr cset 

131 
 UnsatC 

132 
 SatC 

133 
 UnexpandedC _ > () 

134 
in 

135 
graphIterCnstrs cfkt1; 

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

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

138 
setIterState (fun state > stateSetStatus state Sat) setStates; 

139 
let setCoreSat core = 

140 
coreSetStatus core Sat; 

141 
if core == graphGetRoot () then raise (CoAlg_finished true) else () 

142 
in 

143 
setIterCore setCoreSat setCores; 

144 
setIterCnstr (fun cset > graphReplaceCnstr cset SatC) setCnstr 

145  
146  57 
module HashSet = struct 
147  58 
type 'a t = ('a, unit) Hashtbl.t 
148  59  
...  ...  
156  67 
Hashtbl.iter f_intern set 
157  68 
end 
158  69  
159 
let solveGame () = 

160 
let seenOpen = HashSet.create (graphSizeCore ()) in 

161  
162 
let stateGetIdxOr node state = 

163 
match stateGetStatus state with 

164 
 Expandable > 

165 
(match node with  None > stateGetIdx state  Some idx > idx) 

166 
 Sat > PG_Map.sat_node 

167 
 Unsat > PG_Map.unsat_node 

168 
 Open > stateGetIdx state 

169 
in 

170 
let coreGetIdxOr node core = 

171 
match coreGetStatus core with 

172 
 Expandable > 

173 
(match node with  None > coreGetIdx core  Some idx > idx) 

174 
 Sat > PG_Map.sat_node 

175 
 Unsat > PG_Map.unsat_node 

176 
 Open > coreGetIdx core 

177 
in 

178  
179 
let coreGetIdxOr1 core = 

180 
match coreGetStatus core with 

181 
 Expandable > begin match coreGetChildren core with 

182 
 [] > PG_Map.unsat_node 

183 
 _ > coreGetIdx core 

184 
end 

185 
 Sat > PG_Map.sat_node 

186 
 Unsat > PG_Map.unsat_node 

187 
 Open > coreGetIdx core 

188 
in 

189  
190 
let emptyToSat = function 

191 
 [] > [PG_Map.sat_node] 

192 
 x > x 

193 
in 

194  
195 
let nodeSucessors1 node = 

196 
match PG_Map.find node with 

197 
 PG_Map.State state > emptyToSat (List.map fst (stateGetRulesWithIndex state)) 

198 
 PG_Map.Core core > List.map (stateGetIdxOr (Some PG_Map.unsat_node)) (coreGetChildren core) 

199 
 PG_Map.Rule (_,cores) > List.map coreGetIdxOr1 cores 

200 
 PG_Map.Sat > [PG_Map.sat_node] 

201 
 PG_Map.Unsat > [PG_Map.unsat_node] 

202 
in 

203 
let nodeSucessors2 node = 

204 
match PG_Map.find node with 

205 
 PG_Map.State state > emptyToSat (List.map fst (stateGetRulesWithIndex state)) 

206 
 PG_Map.Core core > List.map (stateGetIdxOr (Some PG_Map.sat_node)) (coreGetChildren core) 

207 
 PG_Map.Rule (_,cores) > List.map (coreGetIdxOr (Some PG_Map.sat_node)) cores 

208 
 PG_Map.Sat > [PG_Map.sat_node] 

209 
 PG_Map.Unsat > [PG_Map.unsat_node] 

210 
in 

211  
212 
let eloise = PG.plr_Even in 

213 
let abelard = PG.plr_Odd in 

214  
215 
let nodeData node = 

216 
match PG_Map.find node with 

217 
 PG_Map.State state > 

218 
HashSet.add seenOpen node; 

219 
(T.priority (stateGetFocus state), abelard) 

220 
 PG_Map.Core core > 

221 
HashSet.add seenOpen node; 

222 
(T.priority (coreGetFocus core), eloise) 

223 
 PG_Map.Rule (state,_) > (T.priority (stateGetFocus state), eloise) 

224 
 PG_Map.Sat > (2, eloise) 

225 
 PG_Map.Unsat > (1, abelard) 

226 
in 

227  
228 
let root_idx1 = coreGetIdxOr1 (graphGetRoot ()) in 

229 
let game1 = (root_idx1, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors1, nodeData, fun _ > None) in 

230 
let root_idx2 = coreGetIdxOr (Some PG_Map.sat_node) (graphGetRoot ()) in 

231 
let game2 = (root_idx2, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors2, nodeData, fun _ > None) in 

232 
(* Basics.verbosity := 3; *) 

233  
234 
let seenmap = Hashtbl.create 10 in 

235 
let rec printGame game node = 

236 
if Hashtbl.mem seenmap node then () else 

237 
begin 

238 
Hashtbl.add seenmap node (); 

239 
let (_, suc, _, _) = game in 

240 
let children = Tcsbasedata.Enumerators.to_list (suc node) in 

241 
let formatList l = "[" ^ String.concat "; " (List.map string_of_int l) ^ "]" in 

242 
Printf.printf "%d > %s\n" node (formatList children); 

243 
List.iter (printGame game) children 

244 
end 

245 
in 

246  
247 
(* print_endline "GAME 1 ####################"; *) 

248 
(* printGame game1 root_idx1; *) 

249 
(* print_endline "GAME 2 ####################"; *) 

250 
(* Hashtbl.clear seenmap; *) 

251 
(* printGame game2 root_idx2; *) 

252  
253 
let solution1 = Stratimprlocal2.partially_solve game1 in 

254 
let solution2 = Stratimprlocal2.partially_solve game2 in 

255  
256 
let nodeSetStatus node status = match PG_Map.find node with 

257 
 PG_Map.State state > stateSetStatus state status 

258 
 PG_Map.Core core > coreSetStatus core status 

259 
 _ > assert false 

260 
in 

261 
let applySolution node = 

262 
let (sol1_player,_) = solution1 node in 

263 
let (sol2_player,_) = solution2 node in 

264 
if sol1_player = eloise then begin 

265 
nodeSetStatus node Sat 

266 
end 

267 
else if sol2_player = abelard then begin 

268 
nodeSetStatus node Unsat 

70 
let propagateSatMu () = 

71 
let maxPrio = ref 0 in 

72 
(* get highest priority that occurs in open or expandable states or cores *) 

73 
(* alternative: *) 

74 
(* let maxPrio = (!MiscSolver.nrFormulae * (maxAlternationDepth ()))+2 in *) 

75 
let getMaxPrioStates state = 

76 
let prioState state = T.priority (stateGetFocus state) in 

77 
if (prioState state > !maxPrio) then (maxPrio := prioState state;) 

78 
in 

79 
let getMaxPrioCores core = 

80 
let prioCore core = T.priority (coreGetFocus core) in 

81 
if (prioCore core > !maxPrio) then (maxPrio := prioCore core;) 

82 
in 

83 
graphIterStates getMaxPrioStates; 

84 
graphIterCores getMaxPrioCores; 

85  
86 
let setStates = setEmptyState () in 

87 
let setCores = setEmptyCore () in 

88 
let setStartersStates = setEmptyState () in 

89 
let setStartersCores = setEmptyCore () in 

90 
let openstates = ref 0 in 

91 
let emptySet = bsetMakeRealEmpty () in 

92 
let setsEmptyState ind = Array.init ind (fun _ > setEmptyState ()) in 

93 
let setsEmptyCore ind = Array.init ind (fun _ > setEmptyCore ()) in 

94 
let setsPriorityStates = setsEmptyState ((!maxPrio) + 1) in 

95 
let setsPriorityCores = setsEmptyCore ((!maxPrio) + 1) in 

96  
97 
(* Partition set of nodes according to their priorities 

98 
*) 

99 
let stateCollector state = 

100 
match stateGetStatus state with 

101 
 Unsat > () 

102 
 Sat > () 

103 
 Expandable > () 

104 
 Open > 

105 
openstates := !openstates + 1; 

106 
setAddState (Array.get setsPriorityStates (T.priority (stateGetFocus state))) state; 

107 
setAddState setStates state; 

108 
(* As it is enough for a core to have one child that Eloise wins, we can 

109 
* also handle (some) expandable cores. 

110 
*) 

111 
and coreCollector core = 

112 
match coreGetStatus core with 

113 
 Unsat > () 

114 
 Sat > () 

115 
 Expandable > 

116 
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core; 

117 
setAddCore setCores core; 

118 
 Open > 

119 
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core; 

120 
setAddCore setCores core; 

121 
in 

122 
graphIterStates stateCollector; 

123 
graphIterCores coreCollector; 

124  
125 
setPropagationCounter !openstates; 

126  
127 
let initializeFPStates ind = Array.init ind (fun i > if (i mod 2 == 0) then setStates else (setEmptyState ())) in 

128 
let initializeFPCores ind = Array.init ind (fun i > if (i mod 2 == 0) then setCores else (setEmptyCore ())) in 

129 
let setsFPVarsStates = initializeFPStates ((!maxPrio)+1) in 

130 
let setsFPVarsCores = initializeFPCores ((!maxPrio)+1) in 

131 
let resetLevel = ref 0 in 

132 
if (!maxPrio mod 2 == 1) then resetLevel := !maxPrio + 1 else resetLevel := !maxPrio; 

133 
(* All rule applications need to still be potentially won by Eloise for a 

134 
* State to be a valid startingpoint for this fixpoint. 

135 
*) 

136 
let onestepFunctionState resultStates (state : state) = 

137 
let ruleiter (dependencies, corelist) : bool = 

138 
List.exists (fun (core : core) > coreGetStatus core == Sat  

139 
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core)) corelist 

140 
in 

141 
if (List.for_all ruleiter (stateGetRules state)) then begin 

142 
setAddState resultStates state 

269  143 
end 
270 
in 

271  
272 
HashSet.iter applySolution seenOpen 

273  
274 
(* let propagateSatMu () = *) 

275 
(* let setFinishingStates = setEmptyState () in *) 

276 
(* let setFinishingCores = setEmptyCore () in *) 

277 
(* let setStates = setEmptyState () in *) 

278 
(* let setCores = setEmptyCore () in *) 

279 
(* let emptySet = bsetMakeRealEmpty () in *) 

280 
(* let openstates = ref 0 in *) 

281  
282 
(* (\* Collect two sets of nodes. All nodes that may be satisfiable *) 

283 
(* * after this iteration are collected into setStates/setCores. *) 

284 
(* * *) 

285 
(* * As every cycle containing a node with empty focus or an *) 

286 
(* * satisfiable node should be considered satisfiable, collect these *) 

287 
(* * decisive nodes into setFinishingStates/setFinishingCores *) 

288 
(* * *) 

289 
(* * This also marks in trivial cases nodes as satisfiable. *) 

290 
(* *\) *) 

291 
(* let stateCollector state = *) 

292 
(* match stateGetStatus state with *) 

293 
(*  Unsat > () *) 

294 
(*  Sat > *) 

295 
(* setAddState setStates state; *) 

296 
(* setAddState setFinishingStates state *) 

297 
(*  Expandable > () *) 

298 
(*  Open > *) 

299 
(* openstates := !openstates + 1; *) 

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

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

302 
(* then begin *) 

303 
(* setAddState setFinishingStates state; *) 

304 
(* stateSetStatus state Sat *) 

305 
(* end else begin *) 

306 
(* setAddState setStates state; *) 

307 
(* if bsetCompare (stateGetFocus state) emptySet == 0 *) 

308 
(* then begin *) 

309 
(* setAddState setFinishingStates state *) 

310 
(* end *) 

311 
(* else () *) 

312 
(* end *) 

313  
314 
(* (\* As it is enough for a core to have one successfull child, we can *) 

315 
(* * also handle (some) expandable cores. *) 

316 
(* *\) *) 

317 
(* and coreCollector core = *) 

318 
(* match coreGetStatus core with *) 

319 
(*  Unsat > () *) 

320 
(*  Sat > *) 

321 
(* setAddCore setCores core; *) 

322 
(* setAddCore setFinishingCores core *) 

323 
(*  Expandable *) 

324 
(*  Open > *) 

325 
(* setAddCore setCores core; *) 

326 
(* if bsetCompare (coreGetFocus core) emptySet == 0 *) 

327 
(* then begin *) 

328 
(* setAddCore setFinishingCores core *) 

329 
(* end *) 

330 
(* else () *) 

331 
(* in *) 

332 
(* graphIterStates stateCollector; *) 

333 
(* graphIterCores coreCollector; *) 

334  
335 
(* setPropagationCounter !openstates; *) 

336  
337 
(* (\* In a fixpoint the set called setStates / setCores is narrowed *) 

338 
(* * down. *) 

339 
(* * *) 

340 
(* * In each step only those states and cores are retained in setStates *) 

341 
(* * / setCores which reach one of setFinishing{States,Cores} in *) 

342 
(* * finitely many steps. This new set of States / Cores is collected *) 

343 
(* * as allowed{States,Cores} during each fixpoint iteration. *) 

344 
(* * *) 

345 
(* * Only those finishing nodes are retained that have allowed or *) 

346 
(* * Successfull Children. *) 

347 
(* *\) *) 

348 
(* let rec fixpointstep setStates setCores = *) 

349 
(* let allowedStates = setEmptyState () in *) 

350 
(* let allowedCores = setEmptyCore () in *) 

351  
352 
(* let rec visitParentStates (core : core) : unit = *) 

353 
(* if not (setMemCore allowedCores core) *) 

354 
(* then begin *) 

355 
(* setAddCore allowedCores core; *) 

356 
(* let verifyParent (state,_) = *) 

357 
(* let rules = stateGetRules state in *) 

358 
(* let ruleiter (dependencies, corelist) = *) 

359 
(* List.exists (fun (core : core) > setMemCore allowedCores core  *) 

360 
(* coreGetStatus core == Sat) *) 

361 
(* corelist *) 

362 
(* in *) 

363 
(* if List.for_all ruleiter rules *) 

364 
(* then visitParentCores state *) 

365 
(* in *) 

366 
(* List.iter verifyParent (coreGetParents core) *) 

367 
(* end *) 

368  
369 
(* and visitParentCores (state : state) : unit = *) 

370 
(* if not (setMemState allowedStates state) *) 

371 
(* then begin *) 

372 
(* setAddState allowedStates state; *) 

373 
(* let verifyParent core = *) 

374 
(* let acceptable = *) 

375 
(* List.exists (fun (state : state) > setMemState allowedStates state  *) 

376 
(* stateGetStatus state == Sat) *) 

377 
(* (coreGetChildren core) *) 

378 
(* in *) 

379 
(* if acceptable *) 

380 
(* then visitParentStates core *) 

381 
(* in *) 

382 
(* List.iter verifyParent (stateGetParents state) *) 

383 
(* end *) 

384 
(* in *) 

385  
386 
(* (\* All rule applications need to still be potentially Sat for a *) 

387 
(* * finishing State to be a valid startingpoint for this fixpoint. *) 

388 
(* *\) *) 

389 
(* let checkFinishingState (state : state) = *) 

390 
(* let ruleiter (dependencies, corelist) : bool = *) 

391 
(* List.for_all (fun (core : core) > coreGetStatus core == Unsat  *) 

392 
(* coreGetStatus core == Expandable  *) 

393 
(* not (setMemCore setCores core)) corelist *) 

394 
(* in *) 

395 
(* if not (List.exists ruleiter (stateGetRules state)) then begin *) 

396 
(* visitParentCores state *) 

397 
(* end *) 

398  
399 
(* (\* There needs to be a State still potentially Sat for this core *) 

400 
(* * to be considered for the fixpoint *) 

401 
(* *\) *) 

402 
(* and checkFinishingCore (core : core) = *) 

403 
(* if not (List.for_all (fun (state : state) > stateGetStatus state == Unsat  *) 

404 
(* stateGetStatus state == Expandable  *) 

405 
(* not (setMemState setStates state)) *) 

406 
(* (coreGetChildren core)) *) 

407 
(* then begin *) 

408 
(* visitParentStates core *) 

409 
(* end *) 

410 
(* in *) 

411 
(* setIterState checkFinishingState setFinishingStates; *) 

412 
(* setIterCore checkFinishingCore setFinishingCores; *) 

413  
414  
415 
(* if (setLengthState setStates) = (setLengthState allowedStates) && *) 

416 
(* (setLengthCore setCores) = (setLengthCore allowedCores) *) 

417 
(* then begin *) 

418 
(* setIterState (fun state > stateSetStatus state Sat) setStates; *) 

419 
(* setIterCore (fun core > coreSetStatus core Sat; if core == graphGetRoot () *) 

420 
(* then raise (CoAlg_finished true) *) 

421 
(* else ()) setCores; *) 

422 
(* end else *) 

423 
(* fixpointstep allowedStates allowedCores *) 

424 
(* in *) 

425 
(* fixpointstep setStates setCores *) 

426  
144 


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

146 
* to be considered for the fixpoint. 

147 
*) 

148 
in 

149 
let onestepFunctionCore resultCores (core : core) = 

150 
if (List.exists (fun (state : state) > stateGetStatus state == Sat  

151 
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state))) (coreGetChildren core) 

152 
then begin 

153 
setAddCore resultCores core 

154 
end 

155 
in 

156 


157 
(* given the input arrays of sets (setsFPVars{States,Cores}), compute starters for this 

158 
* vector and then compute nodes for which Eloise can enforce reaching a starter 

159 
*) 

160 
let rec computeFixpoint ind = 

161 
if (ind == 0) then begin 

162 
let resultStates = setEmptyState () in 

163 
let resultCores = setEmptyCore () in 

164 
setIterState (onestepFunctionState resultStates) setStates; 

165 
setIterCore (onestepFunctionCore resultCores) setCores; 

166 
if ((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) && 

167 
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores)) 

168 
then begin 

169 
(resultStates, resultCores) 

170 
end 

171 
else begin 

172 
Array.set setsFPVarsStates ind (resultStates); 

173 
Array.set setsFPVarsCores ind (resultCores); 

174 
computeFixpoint ind 

175 
end 

176 
end 

177 
else begin 

178 
if (ind mod 2 == 1) && (ind < !resetLevel) then begin 

179 
Array.set setsFPVarsStates ind (setEmptyState ()); 

180 
Array.set setsFPVarsCores ind (setEmptyCore ()); 

181 
resetLevel := ind; 

182 
end; 

183 
let (resultStates, resultCores) = computeFixpoint (ind  1) in 

184 
if (((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) && 

185 
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores)))  

186 
((setLengthState (Array.get setsPriorityStates ind) == 0) && (setLengthCore (Array.get setsPriorityCores ind) == 0)) 

187 
then begin 

188 
resetLevel := ind + 1; 

189 
(resultStates, resultCores) 

190 
end 

191 
else begin 

192 
Array.set setsFPVarsStates ind (resultStates); 

193 
Array.set setsFPVarsCores ind (resultCores); 

194 
computeFixpoint ind; 

195 
end 

196 
end 

197 
in 

198 
let (resultStates, resultCores) = computeFixpoint !maxPrio in 

199 
setIterState (fun state > stateSetStatus state Sat) resultStates; 

200 
setIterCore (fun core > coreSetStatus core Sat; if core == graphGetRoot () 

201 
then begin 

202 
raise (CoAlg_finished true) 

203 
end 

204 
else ()) resultCores 

427  205  
428  206 
(*****************************************************************************) 
429  207 
(* Propagation of Unsatisfiability *) 
430  208 
(*****************************************************************************) 
431  209  
432 
let isConstraintUnsat cset = 

433 
match graphFindCnstr cset with 

434 
 None > assert false 

435 
 Some UnsatC > true 

436 
 _ > false 

210 
let propagateUnsatMu () = 

211 
(* let maxPrio = (!MiscSolver.nrFormulae * (maxAlternationDepth ()))+2 in *) 

212 
let maxPrio = ref 0 in 

213 
(* get highest priority that occurs in open or expandable states or cores *) 

214 
let getMaxPrioStates state = 

215 
let prioState state = T.priority (stateGetFocus state) in 

216 
if (prioState state > !maxPrio) then (maxPrio := prioState state;) 

217 
in 

218 
let getMaxPrioCores core = 

219 
let prioCore core = T.priority (coreGetFocus core) in 

220 
if (prioCore core > !maxPrio) then (maxPrio := prioCore core;) 

221 
in 

222 
graphIterStates getMaxPrioStates; 

223 
graphIterCores getMaxPrioCores; 

224 
(* Partition set of nodes according to their priorities 

225 
* 

226 
* This also marks trivially successful nodes. 

227 
*) 

228 
let setStates = setEmptyState () in 

229 
let setCores = setEmptyCore () in 

230 
let setStartersStates = setEmptyState () in 

231 
let setStartersCores = setEmptyCore () in 

232 
let openstates = ref 0 in 

233 
let emptySet = bsetMakeRealEmpty () in 

234 
let setsEmptyState ind = Array.init ind (fun _ > setEmptyState ()) in 

235 
let setsEmptyCore ind = Array.init ind (fun _ > setEmptyCore ()) in 

236 
let setsPriorityStates = setsEmptyState ((!maxPrio) + 1) in 

237 
let setsPriorityCores = setsEmptyCore ((!maxPrio) + 1) in 

238  
239 
let stateCollector state = 

240 
match stateGetStatus state with 

241 
 Sat > () 

242 
 Unsat > () 

243 
 Expandable > () 

244 
 Open > 

245 
openstates := !openstates + 1; 

246 
setAddState (Array.get setsPriorityStates (T.priority (stateGetFocus state))) state; 

247 
setAddState setStates state; 

248 
and coreCollector core = 

249 
match coreGetStatus core with 

250 
 Sat > () 

251 
 Unsat > () 

252 
 Expandable > () 

253 
 Open > 

254 
setAddCore (Array.get setsPriorityCores (T.priority (coreGetFocus core))) core; 

255 
setAddCore setCores core; 

256 
in 

257 
graphIterStates stateCollector; 

258 
graphIterCores coreCollector; 

259  
260 
setPropagationCounter !openstates; 

261  
262 
let initializeFPStates ind = Array.init ind (fun i > if (i mod 2 == 1) then setStates else (setEmptyState ())) in 

263 
let initializeFPCores ind = Array.init ind (fun i > if (i mod 2 == 1) then setCores else (setEmptyCore ())) in 

264 
let setsFPVarsStates = initializeFPStates ((!maxPrio)+1) in 

265 
let setsFPVarsCores = initializeFPCores ((!maxPrio)+1) in 

266 
let resetLevel = ref 0 in 

267 
if (!maxPrio mod 2 == 0) then resetLevel := !maxPrio + 1 else resetLevel := !maxPrio; 

268 
let onestepFunctionState resultStates (state : state) = 

269 
let ruleiter (dependencies, corelist) : bool = 

270 
List.for_all (fun (core : core) > (coreGetStatus core <> Sat) && ( (coreGetStatus core == Unsat)  

271 
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core) )) corelist 

272 
in 

273 
if (List.exists ruleiter (stateGetRules state)) then begin 

274 
setAddState resultStates state 

275 
end 

276 
in 

277 
let onestepFunctionCore resultCores (core : core) = 

278 
if (List.for_all (fun (state : state) > (stateGetStatus state <> Sat) && ((stateGetStatus state == Unsat)  

279 
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state)))) (coreGetChildren core) 

280 
then begin 

281 
setAddCore resultCores core 

282 
end 

283 
in 

284 


285 
let rec computeFixpoint ind = 

286 
if (ind == 0) then begin 

287 
if (ind mod 2 == 0) && (ind < !resetLevel) then begin 

288 
Array.set setsFPVarsStates ind (setEmptyState ()); 

289 
Array.set setsFPVarsCores ind (setEmptyCore ()); 

290 
resetLevel := ind; 

291 
end; 

292 
let resultStates = setEmptyState () in 

293 
let resultCores = setEmptyCore () in 

294 
setIterState (onestepFunctionState resultStates) setStates; 

295 
setIterCore (onestepFunctionCore resultCores) setCores; 

296 
if ((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) && 

297 
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores)) 

298 
then begin 

299 
resetLevel := ind + 1; 

300 
(resultStates, resultCores) 

301 
end 

302 
else begin 

303 
Array.set setsFPVarsStates ind (resultStates); 

304 
Array.set setsFPVarsCores ind (resultCores); 

305 
computeFixpoint ind 

306 
end 

307 
end 

308 
else begin 

309 
if (ind mod 2 == 1) && (ind < !resetLevel) then begin 

310 
Array.set setsFPVarsStates ind (setStates); 

311 
Array.set setsFPVarsCores ind (setCores); 

312 
resetLevel := ind; 

313 
end; 

314 
let (resultStates, resultCores) = computeFixpoint (ind  1) in 

315 
if (((setLengthState (Array.get setsFPVarsStates ind)) == (setLengthState resultStates)) && 

316 
((setLengthCore (Array.get setsFPVarsCores ind)) == (setLengthCore resultCores)))  

317 
((setLengthState (Array.get setsPriorityStates ind) == 0) && (setLengthCore (Array.get setsPriorityCores ind) == 0)) 

318 
then begin 

319 
resetLevel := ind + 1; 

320 
(resultStates, resultCores) 

321 
end 

322 
else begin 

323 
Array.set setsFPVarsStates ind (resultStates); 

324 
Array.set setsFPVarsCores ind (resultCores); 

325 
computeFixpoint ind; 

326 
end 

327 
end 

328 
in 

329 
let (resultStates, resultCores) = computeFixpoint !maxPrio in 

330 
setIterState (fun state > stateSetStatus state Unsat) resultStates; 

331 
setIterCore (fun core > coreSetStatus core Unsat; if core == graphGetRoot () 

332 
then begin 

333 
raise (CoAlg_finished false) 

334 
end 

335 
else ()) resultCores 

336  
337 
(*****************************************************************************) 

338 
(* Node Expansions *) 

339 
(*****************************************************************************) 

437  340  
438  341 
let fhtMustFind fht f = 
439  342 
match fhtFind fht f with 
...  ...  
445  348 
 Some f > f 
446  349 
 None > assert false 
447  350  
448  
449 
(* Gets a list of Things we know are unsatisfiable and propagates this 

450 
information backwards *) 

451 
let rec propagateUnsat = function 

452 
 [] > () 

453 
 propElem::tl > 

454 
let tl1 = 

455 
match propElem with 

456 
 UState (state, idxopt) > begin 

457 
match stateGetStatus state with 

458 
 Unsat > tl 

459 
 Sat > raise (ReasonerError ("Propagation tells state " 

460 
^(string_of_int (stateGetIdx state)) 

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

462 
 Open 

463 
 Expandable > 

464 
let mbs = stateGetBs state 

465 
(* match idxopt with *) 

466 
(*  None > stateGetBs state *) 

467 
(*  Some idx > *) 

468 
(* let (dep, children) = stateGetRule state idx in *) 

469 
(* let getBs core = *) 

470 
(* assert (coreGetStatus core = Unsat); *) 

471 
(* coreGetBs core *) 

472 
(* in *) 

473 
(* dep (List.map getBs children) *) 

474 
in 

475 
stateSetBs state mbs; 

476 
stateSetStatus state Unsat; 

477 
let prop acc core = 

478 
let turnsUnsat = 

479 
match coreGetStatus core with 

480 
 Open > List.for_all (fun s > stateGetStatus s = Unsat) 

481 
(coreGetChildren core) 

482 
 Expandable 

483 
 Unsat 

484 
 Sat > false 

485 
in 

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

487 
in 

488 
List.fold_left prop tl (stateGetParents state) 

489 
end 

490 
 UCore (core, comesFromCnstr) > begin 

491 
match coreGetStatus core with 

492 
 Unsat > tl 

493 
 Sat > raise (ReasonerError ("Propagation tells core " 

494 
^(string_of_int (coreGetIdx core)) 

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

496 
 Open 

497 
 Expandable > 

498 
let mbs = 

499 
if comesFromCnstr then coreGetBs core 

500 
else 

501 
let bs = coreGetBs core in 

502 
let solver = coreGetSolver core in 

503 
let fht = coreGetFht core in 

504 
let lht = lhtInit () in 

505 
let addLits f acc = 

506 
let lit = fhtMustFind fht f in 

507 
lhtAdd lht lit f; 

508 
lit::acc 

509 
in 

510 
let litset = bsetFold addLits bs [] in 

511 
let addClauses state = 

512 
let cbs = stateGetBs state in 

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

514 
let okay = M.add_clause solver clause in 

515 
assert okay 

516 
in 

517 
List.iter addClauses (coreGetChildren core); 

518 
let isSat = M.invoke_solver solver litset in 

519 
assert (not isSat); 

520 
let res = bsetMake () in 

521 
let confls = M.get_conflict solver in 

522 
List.iter (fun l > bsetAdd res (lhtMustFind lht l)) confls; 

523 
res 

524 
in 

525 
coreSetBs core mbs; 

526 
coreSetStatus core Unsat; 

527 
coreDeallocateSolver core; 

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

529 
let prop acc (state, idx) = 

530 
let turnsUnsat = 

531 
match stateGetStatus state with 

532 
 Open 

533 
 Expandable > 

534 
List.for_all (fun c > coreGetStatus c = Unsat) (snd (stateGetRule state idx)) 

535 
 Unsat 

536 
 Sat > false 

537 
in 

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

539 
in 

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

541 
List.fold_left (fun acc cset > (UCnstr cset)::acc) tl2 (coreGetConstraintParents core) 

542 
end 

543 
 UCnstr cset > 

544 
match graphFindCnstr cset with 

545 
 None 

546 
 Some SatC > assert false 

547 
 Some UnsatC > tl 

548 
 Some (UnexpandedC nodes) 

549 
 Some (OpenC nodes) > 

550 
graphReplaceCnstr cset UnsatC; 

551 
let prop acc node = 

552 
match node with 

553 
 State state > 

554 
let turnsUnsat = 

555 
match stateGetStatus state with 

556 
 Expandable 

557 
 Open > cssForall isConstraintUnsat (stateGetConstraints state) 

558 
 Unsat 

559 
 Sat > false 

560 
in 

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

562 
 Core core > 

563 
let turnsUnsat = 

564 
match coreGetStatus core with 

565 
 Expandable 

566 
 Open > cssForall isConstraintUnsat (coreGetConstraints core) 

567 
 Unsat 

568 
 Sat > false 

569 
in 

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

571 
in 

572 
List.fold_left prop tl nodes 

573 
in 

574 
propagateUnsat tl1 

575  
576 
(* let propagateUnsatMu () = *) 

577 
(* let setFinishingStates = setEmptyState () in *) 

578 
(* let setFinishingCores = setEmptyCore () in *) 

579 
(* let setStates = setEmptyState () in *) 

580 
(* let setCores = setEmptyCore () in *) 

581 
(* let emptySet = bsetMakeRealEmpty () in *) 

582  
583 
(* (\* Collect two sets of nodes. All nodes that may be unsatisfiable *) 

584 
(* * after this iteration are collected into setStates/setCores. *) 

585 
(* * *) 

586 
(* * Nodes reaching Points with empty focus as well as Expandable nodes *) 

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

588 
(* * setFinishingStates/setFinishingCores. *) 

589 
(* *\) *) 

590 
(* let stateCollector state = *) 

591 
(* match stateGetStatus state with *) 

592 
(*  Unsat > () *) 

593 
(*  Sat *) 

594 
(*  Expandable > *) 

595 
(* setAddState setStates state; *) 

596 
(* setAddState setFinishingStates state *) 

597 
(*  Open > *) 

598 
(* setAddState setStates state; *) 

599 
(* if [] = (stateGetRules state) *) 

600 
(* then begin *) 

601 
(* stateSetStatus state Sat; *) 

602 
(* setAddState setFinishingStates state *) 

603 
(* end *) 

604 
(* else (); *) 

605 
(* if bsetCompare (stateGetDeferral state) emptySet == 0 *) 

606 
(* then begin *) 

607 
(* setAddState setFinishingStates state *) 

608 
(* end *) 

609 
(* else () *) 

610  
611 
(* and coreCollector core = *) 

612 
(* match coreGetStatus core with *) 

613 
(*  Unsat > () *) 

614 
(*  Expandable *) 

615 
(*  Sat > *) 

616 
(* setAddCore setCores core; *) 

617 
(* setAddCore setFinishingCores core *) 

618 
(*  Open > *) 

619 
(* setAddCore setCores core; *) 

620 
(* if bsetCompare (coreGetDeferral core) emptySet == 0 *) 

621 
(* then begin *) 

622 
(* setAddCore setFinishingCores core *) 

623 
(* end *) 

624 
(* else () *) 

625 
(* in *) 

626 
(* graphIterStates stateCollector; *) 

627 
(* graphIterCores coreCollector; *) 

628  
629 
(* (\* In a fixpoint the set called setFinishingStates/setFinishingCores *) 

630 
(* * is narrowed down *) 

631 
(* * *) 

632 
(* * In each iteration we start with all Nodes and remove all that can *) 

633 
(* * reach a finishing Node. We then remove all finishing Nodes from the *) 

634 
(* * respective set which are becoming Unsat and start with the next *) 

635 
(* * iteration until the fixpoint is reached *) 

636 
(* * *) 

637 
(* * *) 

638 
(* *\) *) 

639 
(* let rec fixpointstep setPrevUnsatStates setPrevUnsatCores = *) 

640 
(* let setUnsatStates = setCopyState setStates in *) 

641 
(* let setUnsatCores = setCopyCore setCores in *) 

642  
643 
(* let rec visitParentStates (core : core) : unit = *) 

644 
(* if setMemCore setUnsatCores core *) 

645 
(* then begin *) 

646 
(* setRemoveCore setUnsatCores core; *) 

647 
(* let verifyParent (state,_) = *) 

648 
(* let rules = stateGetRules state in *) 

649 
(* let ruleiter (dependencies, corelist) = *) 

650 
(* List.exists (fun (core : core) > not (setMemCore setUnsatCores core)  *) 

651 
(* coreGetStatus core == Sat) *) 

652 
(* corelist *) 

653 
(* in *) 

654 
(* if List.for_all ruleiter rules *) 

655 
(* then visitParentCores state *) 

656 
(* in *) 

657 
(* List.iter verifyParent (coreGetParents core) *) 

658 
(* end *) 

659  
660 
(* and visitParentCores (state : state) : unit = *) 

661 
(* if setMemState setUnsatStates state *) 

662 
(* then begin *) 

663 
(* setRemoveState setUnsatStates state; *) 

664 
(* let verifyParent core = *) 

665 
(* let acceptable = *) 

666 
(* List.exists (fun (state : state) > not (setMemState setUnsatStates state)  *) 

667 
(* stateGetStatus state == Sat) *) 

668 
(* (coreGetChildren core) *) 

669 
(* in *) 

670 
(* if acceptable *) 

671 
(* then visitParentStates core *) 

672 
(* in *) 

673 
(* List.iter verifyParent (stateGetParents state) *) 

674 
(* end *) 

675 
(* in *) 

676  
677 
(* (\* All rule applications need to still be potentially Sat for a *) 

678 
(* * finishing State to be a valid startingpoint for this fixpoint. *) 

679 
(* *\) *) 

680 
(* let checkFinishingState (state : state) = *) 

681 
(* let ruleiter (dependencies, corelist) : bool = *) 

682 
(* List.for_all (fun (core : core) > coreGetStatus core == Unsat  *) 

683 
(* setMemCore setPrevUnsatCores core) corelist *) 

684 
(* in *) 

685 
(* if not (List.exists ruleiter (stateGetRules state))  *) 

686 
(* stateGetStatus state == Expandable then begin *) 

687 
(* visitParentCores state *) 

688 
(* end *) 

689  
690 
(* (\* There needs to be a State still potentially Sat for this core *) 

691 
(* * to be considered for the fixpoint *) 

692 
(* *\) *) 

693 
(* and checkFinishingCore (core : core) = *) 

694 
(* if not (List.for_all (fun (state : state) > stateGetStatus state == Unsat  *) 

695 
(* setMemState setPrevUnsatStates state) *) 

696 
(* (coreGetChildren core))  *) 

697 
(* coreGetStatus core == Expandable *) 

698 
(* then begin *) 

699 
(* visitParentStates core *) 

700 
(* end *) 

701 
(* in *) 

702 
(* setIterState checkFinishingState setFinishingStates; *) 

703 
(* setIterCore checkFinishingCore setFinishingCores; *) 

704  
705 
(* if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) && *) 

706 
(* (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores) *) 

707 
(* then begin *) 

708 
(* setIterState (fun state > stateSetStatus state Unsat) setUnsatStates; *) 

709 
(* setIterCore (fun core > propagateUnsat [UCore (core, false)]) setUnsatCores; *) 

710 
(* end else *) 

711 
(* fixpointstep setUnsatStates setUnsatCores *) 

712 
(* in *) 

713 
(* fixpointstep (setEmptyState ()) (setEmptyCore ()) *) 

714  
715  
716 
(*****************************************************************************) 

717 
(* Propagation of Nominal Constraints *) 

718 
(*****************************************************************************) 

719  
720 
let extractAts sort bs = 

721 
let ats = csetMake () in 

722 
let procNom nom f = 

723 
match lfGetType sort f with 

724 
 AndF 

725 
 OrF > () 

726 
 TrueFalseF 

727 
 AtF > () 

728 
 _ > csetAdd ats (lfGetAt (sort, nom) f) 

729 
in 

730 
let getAts f = 

731 
match lfGetType sort f with 

732 
 AtF > csetAdd ats (lfToAt sort f) 

733 
 NomF > bsetIter (fun f1 > procNom f f1) bs 

734 
 _ > () 

735 
in 

736 
bsetIter getAts bs; 

737 
ats 

738  
739 
let detConstraintsState state = 

740 
let procRule accR (_, chldrn) = 

741 
let procChldrn accC core = 

742 
if coreGetStatus core = Unsat then accC 

743 
else cssUnion accC (coreGetConstraints core) 

744 
in 

745 
let orset = List.fold_left procChldrn cssEmpty chldrn in 

746 
let procOrset csetO accO = 

747 
let mkUnion csetU accU = 

748 
let cset = csetUnion csetO csetU in 

749 
cssAdd cset accU 

750 
in 

751 
cssFold mkUnion accR accO 

752 
in 

753 
cssFold procOrset orset cssEmpty 

754 
in 

755 
let sort = stateGetSort state in 

756 
let bs = stateGetBs state in 

757 
let ats = extractAts sort bs in 

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

759 
List.fold_left procRule (cssSingleton ats) (stateGetRules state) 

760  
761 
let detConstraintsCore core = 

762 
let sort = coreGetSort core in 

763 
let bs = coreGetBs core in 

764 
let ats = extractAts sort bs in 

765 
let addCnstr acc state = 

766 
if stateGetStatus state = Unsat then acc 

767 
else 

768 
let csets = stateGetConstraints state in 

769 
(* cssFold (fun c a > cssAdd (csetUnion c ats) a) csets acc *) 

770 
cssUnion csets acc 

771 
in 

772 
let initInner = 

773 
if coreGetStatus core = Expandable then 

774 
(* let cset = csetCopy ats in *) 

775 
let cset = ats in 

776 
csetAddDot cset; 

777 
cssSingleton cset 

778 
else cssEmpty 

779 
in 

780 
List.fold_left addCnstr initInner (coreGetChildren core) 

781  
782 
let rec propNom = function 

783 
 [] > () 

784 
 node::tl > 

785 
let tl1 = 

786 
match node with 

787 
 State state > 

788 
if stateGetStatus state = Unsat then tl 

789 
else 

790 
let csets = detConstraintsState state in 

791 
let oldcsets = stateGetConstraints state in 

792 
if cssEqual csets oldcsets then tl 

793 
else begin 

794 
stateSetConstraints state csets; 

795 
List.fold_left (fun acc c > (Core c)::acc) tl (stateGetParents state) 

796 
end 

797 
 Core core > 

798 
if coreGetStatus core = Unsat then tl 

799 
else 

800 
let csets = detConstraintsCore core in 

801 
let oldcsets = coreGetConstraints core in 

802 
if cssEqual csets oldcsets then tl 

803 
else begin 

804 
coreSetConstraints core csets; 

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

806 
end 

807 
in 

808 
propNom tl1 

809  
810 
let updateConstraints node elemU csets = 

811 
let update cset acc = 

812 
let cnstr = 

813 
match graphFindCnstr cset with 

814 
 Some cn > cn 

815 
 None > 

816 
let cn = UnexpandedC [] in 

817 
graphInsertCnstr cset cn; 

818 
queueInsertCnstr cset; 

819 
cn 

820 
in 

821 
match cnstr with 

822 
 UnsatC > acc 

823 
 UnexpandedC parents > 

824 
graphReplaceCnstr cset (UnexpandedC (node::parents)); 

825 
false 

826 
 OpenC parents > 

827 
graphReplaceCnstr cset (OpenC (node::parents)); 

828 
false 

829 
 SatC > false 

830 
in 

831 
let isUnsat = cssFold update csets true in 

832 
if isUnsat then propagateUnsat [elemU] else () 

833  
834 
let propagateNominals () = 

835 
let init = cssSingleton (csetMake ()) in 

836 
graphIterStates (fun s > if stateGetStatus s = Unsat then () else stateSetConstraints s init); 

837 
graphIterCores (fun c > if coreGetStatus c = Unsat then () else coreSetConstraints c init); 

838 
graphIterStates (fun s > propNom [State s]); 

839 
graphIterCores (fun c > propNom [Core c]); 

840 
graphClearCnstr (); 

841 
let fktS state = 

842 
if stateGetStatus state = Unsat then () 

843 
else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state) 

844 
in 

845 
graphIterStates fktS; 

846 
let fktC core = 

847 
if coreGetStatus core = Unsat then () 

848 
else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core) 

849 
in 

850 
graphIterCores fktC 

851  
852  
853 
(*****************************************************************************) 

854 
(* Node Expansions *) 

855 
(*****************************************************************************) 

856  
857  351 
let getLit sort fht solver f = 
858  352 
match fhtFind fht f with 
859  353 
 Some lit > lit 
...  ...  
940  434 
an simple forward implication that could be optimised out 
941  435 
though not without nontrivial transformation of code 
942  436  
943 
f = μ X . φ > lf


944 
φ[X > f] > lf1


437 
f = \u03bc X . \u03c6 > lf


438 
\u03c6[X > f] > lf1


945  439  
946  440 
Then adding lf > lf1 to minisat 
947  441 
*) 
...  ...  
1068  562 
let isUnsat = List.for_all (fun s > stateGetStatus s = Unsat) (coreGetChildren core) in 
1069  563 
if isUnsat 
1070  564 
then 
1071 
propagateUnsat [UCore (core, false)]


565 
coreSetStatus core Unsat


1072  566 
else 
1073  567 
coreSetStatus core Open 
1074  568  
...  ...  
1105  599 
let idx = stateAddRule state dep cores in 
1106  600 
List.iter (fun c > coreAddParent c state idx) cores; 
1107  601 
if List.for_all (fun core > coreGetStatus core = Unsat) cores then begin 
1108 
propagateUnsat [UState (state, Some idx)];


602 
stateSetStatus state Unsat;


1109  603 
true 
1110  604 
end else 
1111  605 
false 
...  ...  
1137  631 
 NoMoreElements > 
1138  632 
setSatOrOpen () 
1139  633  
1140  
1141  634 
let expandCnstr cset = 
1142  635 
let nht = nhtInit () in 
1143  636 
let mkCores f = 
...  ...  
1157  650 
in 
1158  651 
csetIter cset mkCores; 
1159  652 
let inCores (sort, _) bs (isUns, acc) = 
1160 
let core = insertCore sort bs (T.init sort bs) in (* TODO: think of deferral / μ stuff here *)


653 
let core = insertCore sort bs (T.init sort bs) in 

1161  654 
coreAddConstraintParent core cset; 
1162  655 
(coreGetStatus core = Unsat  isUns, core::acc) 
1163  656 
in 
1164  657 
let (isUnsat, children) = nhtFold inCores nht (false, []) in 
1165 
if isUnsat then propagateUnsat [UCnstr cset]


658 
if isUnsat then ()


1166  659 
else 
1167  660 
match graphFindCnstr cset with 
1168  661 
 Some (UnexpandedC parents) > graphReplaceCnstr cset (OpenC parents) 
...  ...  
1178  671 
 QState state > 
1179  672 
if stateGetStatus state = Expandable then begin 
1180  673 
expandState state; 
1181 
if doNominalPropagation () then begin 

1182 
(* propagateNominals (); *) 

1183 
if doSatPropagation () then (solveGame ()) 

1184 
end else () 

674 
if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; 

1185  675 
end else (); 
1186  676 
recursiveAction () 
1187  677 
 QCore core > 
1188  678 
if coreGetStatus core = Expandable then begin 
1189  679 
expandCore core; 
1190 
if doNominalPropagation () then begin 

1191 
(* propagateNominals (); *) 

1192 
if doSatPropagation () then (solveGame ()) 

1193 
end else () 

680 
if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; 

1194  681 
end else (); 
1195  682 
recursiveAction () 
1196  683 
 QCnstr cset > 
...  ...  
1201  688 
let runReasonerStep () = 
1202  689 
let void () = () in 
1203  690 
expandNodesLoop void; (* expand at most one node *) 
1204 
solveGame (); 

691 
propagateSatMu (); 

692 
propagateUnsatMu (); 

1205  693 
(* if this emptied the queue *) 
1206  694 
if queueIsEmpty () then begin 
1207 
(* then check whether the nominals would add further queue elements *) 

1208 
(* print_endline "Propagating nominals..."; *) 

1209 
(* propagateNominals () *) 

1210  695 
end else () (* else: the next step would be to expand another node *) 
1211  696  
1212  697 
let rec buildGraphLoop () = 
1213  698 
let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in 
1214  699 
expandNodesFurther (); (* expand as many queue elements as possible *) 
1215 
(* propagateNominals (); *) 

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

1217  700 
if queueIsEmpty () then () else buildGraphLoop () 
1218  701  
1219  702 
let initReasoner fragSpec sorts nomTable tbox sf = 
...  ...  
1262  745 
let sat = 
1263  746 
try 
1264  747 
buildGraphLoop (); 
1265 
solveGame (); 

748 
propagateSatMu (); 

749 
propagateUnsatMu (); 

750 
(* print_endline ("Tableau fully expanded, final propagation gave no winner! "); *) 

1266  751 
(* get whether the root is satisfiable *) 
1267  752 
(* we know that the reasoner finished, so the value is there, *) 
1268  753 
(* i.e. isRootSat() will give a "Some x" and not "None" *) 
Also available in: Unified diff