cool / src / lib / CoAlgReasoner.ml @ e765822b
History  View  Annotate  Download (28.8 KB)
1 
(** A graphtableaubased decision procedure framework for coalgebraic logics. 

2 
@author Florian Widmann, Daniel Hausmann 
3 
*) 
4  
5 
open CoAlgMisc 
6 
open FocusTracking 
7  
8 
module M = Minisat 
9 
module CU = CoolUtils 
10 
module PG = Paritygame 
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 
module type S = sig 
23 
module G : CoolGraph.S 
24 
val isSat : ?verbose:bool > CoAlgMisc.fragment_spec > sortTable 
25 
> (string > CoAlgFormula.sort option) > 
26 
CoAlgFormula.sortedFormula list > CoAlgFormula.sortedFormula > bool 
27  
28  
29 
val initReasoner : CoAlgMisc.fragment_spec > sortTable 
30 
> (string > CoAlgFormula.sort option) > 
31 
CoAlgFormula.sortedFormula list 
32 
> CoAlgFormula.sortedFormula > unit 
33  
34 
(** Run a single step of the reasoner. That is: Expand one node and perform sat 
35 
propagation. 
36  
37 
This is used in the debugger. 
38 
*) 
39 
val runReasonerStep : unit > unit 
40  
41 
val reasonerFinished : unit > bool 
42 
val isRootSat : unit > bool option 
43  
44 
end 
45  
46 
module Make(T : FocusTracker) = struct 
47 
module G = CoolGraph.Make(T) 
48 
module Logics = CoAlgLogics.Make(T) 
49 

50 
open G 
51 
module PG_Map = ParityGameMapping 
52  
53 
(*****************************************************************************) 
54 
(* Propagation of Satisfiability *) 
55 
(*****************************************************************************) 
56  
57 
module HashSet = struct 
58 
type 'a t = ('a, unit) Hashtbl.t 
59  
60 
let create size = Hashtbl.create size 
61  
62 
let add set value = 
63 
Hashtbl.replace set value () 
64  
65 
let iter f set = 
66 
let f_intern k _ = f k in 
67 
Hashtbl.iter f_intern set 
68 
end 
69  
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 
143 
end 
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 
205  
206 
(*****************************************************************************) 
207 
(* Propagation of Unsatisfiability *) 
208 
(*****************************************************************************) 
209  
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 
(*****************************************************************************) 
340  
341 
let fhtMustFind fht f = 
342 
match fhtFind fht f with 
343 
 Some l > l 
344 
 None > assert false 
345  
346 
let lhtMustFind lht l = 
347 
match lhtFind lht l with 
348 
 Some f > f 
349 
 None > assert false 
350  
351 
let getLit sort fht solver f = 
352 
match fhtFind fht f with 
353 
 Some lit > lit 
354 
 None > 
355 
let var = M.new_variable solver in 
356 
let lit = M.var_to_lit var true in 
357 
fhtAdd fht f lit; 
358 
let () = 
359 
match lfGetNeg sort f with 
360 
 None > () 
361 
 Some nf > 
362 
let nlit = M.neg_lit lit in 
363 
fhtAdd fht nf nlit; 
364 
in 
365 
lit 
366  
367 
let newCore sort bs defer = 
368 
(* when creating a now core from a set of formulas bs 
369 
bs = { x_1, ...., x_n } 
370 
= "x_1 /\ .... /\ x_n" 
371 
Then we do this by: 
372  
373 
1. creating a new literal in the sat solver for each 
374 
"boolean subformula" from the x_i. "boolean subformula" means that 
375 
this subformula is not hidden under modalities but only under 
376 
boolean connectives (/\, \/). 
377 
2. encoding the relation between a formula and its intermediate boolean 
378 
subformulas by a clause: 
379 
*) 
380 
let fht = fhtInit () in 
381 
let solver = M.new_solver () in 
382 
let rec addClauses f = 
383 
(* step 1: create a literal in the satsolver representing the formula f *) 
384 
let lf = getLit sort fht solver f in 
385 
(* step 2: encode relation to possible subformulas *) 
386 
match lfGetType sort f with 
387 
 OrF > 
388 
(* 
389 
case 2.(a) f = f1 \/ f2 
390 
fill fht such that it says: 
391  
392 
f > lf 
393 
f1 > lf1 
394 
f2 > lf2 
395 
*) 
396 
let f1 = lfGetDest1 sort f in 
397 
let f2 = lfGetDest2 sort f in 
398 
addClauses f1; 
399 
addClauses f2; 
400 
let lf1 = fhtMustFind fht f1 in 
401 
let lf2 = fhtMustFind fht f2 in 
402 
(* 
403 
encode the structure of f by adding the clause (lf > lf1 \/ lf2) 
404 
*) 
405 
let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in 
406 
assert (okay) 
407 
 AndF > 
408 
(* 
409 
case 2.(b) f = f1 /\ f2 
410 
fill fht such that it says: 
411  
412 
f > lf 
413 
f1 > lf1 
414 
f2 > lf2 
415 
*) 
416 
let f1 = lfGetDest1 sort f in 
417 
let f2 = lfGetDest2 sort f in 
418 
addClauses f1; 
419 
addClauses f2; 
420 
let lf1 = fhtMustFind fht f1 in 
421 
let lf2 = fhtMustFind fht f2 in 
422 
(* 
423 
encode the structure of f by adding the clauses 
424 
(lf > lf1) /\ (lf > lf2) 
425 
*) 
426 
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in 
427 
assert (okay1); 
428 
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in 
429 
assert (okay2) 
430 
 MuF 
431 
 NuF > 
432 
(* 
433 
Dest of a fixpoint is it's unfolded version. This adds just 
434 
an simple forward implication that could be optimised out 
435 
though not without nontrivial transformation of code 
436  
437 
f = \u03bc X . \u03c6 > lf 
438 
\u03c6[X > f] > lf1 
439  
440 
Then adding lf > lf1 to minisat 
441 
*) 
442 
let f1 = lfGetDest1 sort f in 
443 
addClauses f1; 
444 
let lf1 = fhtMustFind fht f1 in 
445 
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in 
446 
assert (okay1); 
447 
 _ > () 
448 
(* case 2.(c) 
449 
We don't need to do anything except adding f to the fht 
450 
*) 
451 
in 
452 
bsetIter addClauses bs; 
453 
coreMake sort bs defer (Some solver) fht 
454  
455 
let getNextState core = 
456 
(* Create a new state, which is obtained by a satisfying assignment of the 
457 
literals of the minisat solver. 
458 
In addition to that, feed the negation of the satisfying assignment back 
459 
to the minisat solver in order to obtain different solutions on successive 
460 
minisat calls. 
461 
*) 
462 
let bs = coreGetBs core in 
463 
let focus = T.make_transient (coreGetFocus core) in 
464 
let fht = coreGetFht core in 
465 
let litset = bsetFold (fun f acc > (fhtMustFind fht f)::acc) bs [] in 
466 
let solver = coreGetSolver core in 
467 
let isSat = M.invoke_solver solver litset in 
468 
(* Clearly, if the current core is unsatisfiable, no further child state can 
469 
be created *) 
470 
if not isSat then None 
471 
else 
472 
let sort = coreGetSort core in 
473 
(* create a new set of formulas newbs with the property: 
474 
if the conjunction of newbs is satisfiable, then the present core is 
475 
satisfiable. 
476 
*) 
477 
let newbs = bsetMake () in 
478 
(* if newbs = { l_1, .... l_n }, i.e. 
479  
480 
newbs = l_1 /\ ... /\ l_n 
481  
482 
then we can get essentially different satisfying assignments of bs by 
483 
adding another clause 
484  
485 
clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n 
486  
487 
By mkExclClause, newbs is filled, and clause is built in the accumulator acc. 
488 
*) 
489 
let rec mkExclClause tracker f acc = 
490 
(* f is a formula that is true in the current satisfying assignment *) 
491 
match lfGetType sort f with 
492 
 OrF > 
493 
(* if f is true and a disjunction, then one of its disjuncts is true *) 
494 
let f1 = lfGetDest1 sort f in 
495 
let lf1 = fhtMustFind fht f1 in 
496 
(* if the first disjunct f1 is true, then we need to add subformulas 
497 
of f1 to newbs&clause *) 
498 
if M.literal_status solver lf1 = M.LTRUE then 
499 
mkExclClause (T.track1 tracker f1) f1 acc 
500 
else 
501 
(* otherwise f2 must be true *) 
502 
let f2 = lfGetDest2 sort f in 
503 
let lf2 = fhtMustFind fht f2 in 
504 
assert (M.literal_status solver lf2 = M.LTRUE); 
505 
mkExclClause (T.track1 tracker f2) f2 acc 
506 
 AndF > 
507 
(* if the true f is a conjuction, then both conjunctions must be true *) 
508 
let f1 = lfGetDest1 sort f in 
509 
let lf1 = fhtMustFind fht f1 in 
510 
assert (M.literal_status solver lf1 = M.LTRUE); 
511 
let acc1 = mkExclClause (T.track1 tracker f1) f1 acc in 
512 
let f2 = lfGetDest2 sort f in 
513 
let lf2 = fhtMustFind fht f2 in 
514 
assert (M.literal_status solver lf2 = M.LTRUE); 
515 
mkExclClause (T.track1 tracker f2) f2 acc1 
516 
 MuF 
517 
 NuF > 
518 
let f1 = lfGetDest1 sort f in 
519 
mkExclClause (T.track1 tracker f1) f1 acc 
520 
 _ > 
521 
(* if f is a trivial formula or modality, then add it ... *) 
522 
(* ... to newbs *) 
523 
bsetAdd newbs f; 
524 
T.apply tracker focus; 
525 
(* ... and to the new clause *) 
526 
(M.neg_lit (fhtMustFind fht f))::acc 
527 
in 
528 
let init_clause f acc = 
529 
let tracker = T.begin_tracking (coreGetFocus core) focus sort f in 
530 
mkExclClause tracker f acc 
531 
in 
532 
let clause = bsetFold init_clause bs [] in 
533 
let okay = M.add_clause solver clause in 
534 
assert (okay); 
535 
Some (sort, newbs, T.finalize focus) 
536  
537 
let newState sort bs focus = 
538 
let (func, sl) = !sortTable.(sort) in 
539 
let producer = Logics.getExpandingFunctionProducer func in 
540 
let exp = producer sort bs focus sl in 
541 
stateMake sort bs focus exp 
542  
543 
let insertState parent sort bs focus = 
544 
let child = 
545 
match graphFindState sort (bs, focus) with 
546 
 None > 
547 
let s = newState sort bs focus in 
548 
graphInsertState sort (bs, focus) s; 
549 
queueInsertState s; 
550 
s 
551 
 Some s > s 
552 
in 
553 
coreAddChild parent child; 
554 
stateAddParent child parent 
555  
556 
let expandCore core = 
557 
match getNextState core with 
558 
 Some (sort, bs, focus) > 
559 
insertState core sort bs focus; 
560 
queueInsertCore core 
561 
 None > 
562 
let isUnsat = List.for_all (fun s > stateGetStatus s = Unsat) (coreGetChildren core) in 
563 
if isUnsat 
564 
then 
565 
coreSetStatus core Unsat 
566 
else 
567 
coreSetStatus core Open 
568  
569  
570 
let insertCore sort bs focus = 
571 
match graphFindCore sort (bs, focus) with 
572 
 None > 
573 
let c = newCore sort bs focus in 
574 
graphInsertCore sort (bs, focus) c; 
575 
queueInsertCore c; 
576 
c 
577 
 Some c > c 
578  
579 
(** Insert cores for the children generated by a modal rule application. 
580 
* 
581 
* @return true if all new cores are already unsatisfiable, false otherwise 
582 
*) 
583 
let insertRule state dep chldrn = 
584 
let chldrn = listFromLazylist chldrn in 
585 
let mkCores (sort, bs, defer) = 
586 
let bs1 = bsetAddTBox sort bs in 
587 
(* For the aconjunctive fragment, instead of adding a core annotated with 
588 
* all deferrals, we add a core for each formula in the deferral set. *) 
589 
let deferSingletons = [defer] in 
590 
List.map (insertCore sort (bsetCopy bs1)) deferSingletons 
591 
in 
592 
(* A list of cores for each child: [[child1a;child1b]; [child2a;child2b]] *) 
593 
let coresPerChild = List.map mkCores chldrn in 
594 
(* All combinations that take a core from each child: 
595 
* [[ch1a;ch2a]; [ch1a;ch2b]; [ch1b;ch2a]; [ch1b;ch2b]] 
596 
* Neccesary because stateAddRule expects each child to have only one core. *) 
597 
let coresPerRule = CU.TList.combinations coresPerChild in 
598 
let addRule cores = 
599 
let idx = stateAddRule state dep cores in 
600 
List.iter (fun c > coreAddParent c state idx) cores; 
601 
if List.for_all (fun core > coreGetStatus core = Unsat) cores then begin 
602 
stateSetStatus state Unsat; 
603 
true 
604 
end else 
605 
false 
606 
in 
607 
List.mem true (List.map (fun r > addRule r) coresPerRule) 
608 

609  
610 
(** Call insertRule on all rules 
611 
* @return true if any rule application generated only unsat cores 
612 
*) 
613 
let rec insertAllRules state rules = 
614 
List.mem true (List.map (fun (dep, children) > insertRule state dep children) rules) 
615  
616 
let expandState state = 
617 
let setSatOrOpen () = 
618 
if CU.TList.empty (stateGetRules state) then 
619 
stateSetStatus state Sat 
620 
else 
621 
stateSetStatus state Open 
622 
in 
623  
624 
match stateNextRule state with 
625 
 MultipleElements rules > 
626 
let unsat = insertAllRules state rules in 
627 
if not unsat then setSatOrOpen () 
628 
 SingleElement (dep, chldrn) > 
629 
let unsat = insertRule state dep chldrn in 
630 
if not unsat then queueInsertState state else () 
631 
 NoMoreElements > 
632 
setSatOrOpen () 
633  
634 
let expandCnstr cset = 
635 
let nht = nhtInit () in 
636 
let mkCores f = 
637 
let (sort, lf) as nom = atFormulaGetNominal f in 
638 
let nomset = 
639 
match nhtFind nht nom with 
640 
 Some ns > ns 
641 
 None > 
642 
let cset1 = csetCopy cset in 
643 
csetRemDot cset1; 
644 
let bs = csetAddTBox sort cset1 in 
645 
bsetAdd bs lf; 
646 
nhtAdd nht nom bs; 
647 
bs 
648 
in 
649 
bsetAdd nomset (atFormulaGetSubformula f) 
650 
in 
651 
csetIter cset mkCores; 
652 
let inCores (sort, _) bs (isUns, acc) = 
653 
let core = insertCore sort bs (T.init sort bs) in 
654 
coreAddConstraintParent core cset; 
655 
(coreGetStatus core = Unsat  isUns, core::acc) 
656 
in 
657 
let (isUnsat, children) = nhtFold inCores nht (false, []) in 
658 
if isUnsat then () 
659 
else 
660 
match graphFindCnstr cset with 
661 
 Some (UnexpandedC parents) > graphReplaceCnstr cset (OpenC parents) 
662 
 _ > assert false 
663  
664  
665 
(*****************************************************************************) 
666 
(* The Main Loop *) 
667 
(*****************************************************************************) 
668  
669 
let expandNodesLoop (recursiveAction: unit > unit) = 
670 
match queueGetElement () with 
671 
 QState state > 
672 
if stateGetStatus state = Expandable then begin 
673 
expandState state; 
674 
if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; 
675 
end else (); 
676 
recursiveAction () 
677 
 QCore core > 
678 
if coreGetStatus core = Expandable then begin 
679 
expandCore core; 
680 
if doSatPropagation () then begin propagateSatMu (); propagateUnsatMu () end; 
681 
end else (); 
682 
recursiveAction () 
683 
 QCnstr cset > 
684 
expandCnstr cset; 
685 
recursiveAction () 
686 
 QEmpty > () 
687  
688 
let runReasonerStep () = 
689 
let void () = () in 
690 
expandNodesLoop void; (* expand at most one node *) 
691 
propagateSatMu (); 
692 
propagateUnsatMu (); 
693 
(* if this emptied the queue *) 
694 
if queueIsEmpty () then begin 
695 
end else () (* else: the next step would be to expand another node *) 
696  
697 
let rec buildGraphLoop () = 
698 
let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in 
699 
expandNodesFurther (); (* expand as many queue elements as possible *) 
700 
if queueIsEmpty () then () else buildGraphLoop () 
701  
702 
let initReasoner fragSpec sorts nomTable tbox sf = 
703 
sortTable := Array.copy sorts; 
704 
let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in 
705 
let sort = fst sf in 
706 
let bs1 = bsetAddTBox sort bs in 
707 
let focus = T.init sort bs in 
708 
graphInit (); 
709 
queueInit (); 
710 
PG_Map.reset (); 
711 
let root = insertCore sort bs1 focus in 
712 
graphAddRoot root 
713  
714 
let isRootSat () = 
715 
match coreGetStatus (graphGetRoot ()) with 
716 
 Expandable > None 
717 
 Unsat > Some false 
718 
 Sat > Some true 
719 
 Open > if (queueIsEmpty()) then Some true else None 
720  
721 
let reasonerFinished () = 
722 
match coreGetStatus (graphGetRoot ()) with 
723 
 Expandable > false 
724 
 Unsat 
725 
 Sat > true 
726 
 Open > queueIsEmpty () 
727  
728  
729 
(** A graphtableaubased decision procedure framework for coalgebraic logics. 
730 
@param verbose An optional switch which determines 
731 
whether the procedure shall print some information on the standard output. 
732 
The default is false. 
733 
@param sorts An array mapping each sort (represented as an integer) 
734 
to a functor and a list of sorts which are the arguments of the functor. 
735 
@param nomTable A partial function mapping nominals (represented as strings) 
736 
to their sorts. 
737 
@param tbox A list of sorted formulae. 
738 
@param sf A sorted formula. 
739 
@return True if sf is satisfiable wrt tbox, false otherwise. 
740 
*) 
741  
742 
let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf = 
743 
let start = if verbose then Unix.gettimeofday () else 0. in 
744 
initReasoner fragSpec sorts nomTable tbox sf; 
745 
let sat = 
746 
try 
747 
buildGraphLoop (); 
748 
propagateSatMu (); 
749 
propagateUnsatMu (); 
750 
(* print_endline ("Tableau fully expanded, final propagation gave no winner! "); *) 
751 
(* get whether the root is satisfiable *) 
752 
(* we know that the reasoner finished, so the value is there, *) 
753 
(* i.e. isRootSat() will give a "Some x" and not "None" *) 
754 
CU.fromSome (isRootSat()) 
755 
with CoAlg_finished res > res 
756 
in 
757 
(* print some statistics *) 
758 
if verbose then 
759 
let stop = Unix.gettimeofday () in 
760 
let addup lst = List.fold_left (fun acc sf > acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in 
761 
print_newline (); 
762 
print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf)); 
763 
let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in 
764 
print_endline ("Added Size: " ^ (string_of_int size)); 
765 
(* 
766 
print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1)); 
767 
let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in 
768 
print_endline ("Added Size: " ^ (string_of_int nsize)); 
769 
*) 
770 
print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable."); 
771 
print_endline ("Time: " ^ (string_of_float (stop . start))); 
772 
print_endline ("Generated states: " ^ (string_of_int (graphSizeState ()))); 
773 
print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ()))); 
774 
print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ()))); 
775 
print_newline () 
776 
else (); 
777 
sat 
778  
779 
end 
780 
(* vim: set et sw=2 sts=2 ts=8 : *) 