Project

General

Profile

Revision e765822b src/lib/CoAlgReasoner.ml

View differences:

src/lib/CoAlgReasoner.ml
1 1
(** A graph-tableau-based 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