Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ e765822b

History | View | Annotate | Download (28.8 KB)

1
(** A graph-tableau-based 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 graph-tableau-based 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 : *)