Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 92102c11

History | View | Annotate | Download (33.6 KB)

1
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
open CoAlgMisc
7

    
8
module M = Minisat
9

    
10
module CU = CoolUtils
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
(*****************************************************************************)
23
(*                     Propagation of Satisfiability                         *)
24
(*****************************************************************************)
25

    
26
let propSatFindSucc setCnstr cset =
27
  if csetHasDot cset then false
28
  else
29
    match graphFindCnstr cset with
30
    | None -> raise (ReasonerError "?")
31
    | Some SatC -> true
32
    | Some (OpenC _) -> setMemCnstr setCnstr cset
33
    | Some (UnexpandedC _)
34
    | Some UnsatC -> false
35

    
36

    
37
let rec propSat setStates setCores setCnstr = function
38
  | [] -> ()
39
  | propElem::tl ->
40
      let tl1 =
41
        match propElem with
42
        | UState (state, _) ->
43
            if setMemState setStates state then
44
              let cnstrs = stateGetConstraints state in
45
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
46
              if isStillOpen then () else setRemoveState setStates state
47
            else ();
48
            tl
49
        | UCore (core, _) ->
50
            if setMemCore setCores core then
51
              let cnstrs = coreGetConstraints core in
52
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
53
              if isStillOpen then tl else begin
54
                setRemoveCore setCores core;
55
                let cnstrPar = coreGetConstraintParents core in
56
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl cnstrPar
57
              end
58
            else tl
59
        | UCnstr cset ->
60
            if setMemCnstr setCnstr cset then begin
61
              setRemoveCnstr setCnstr cset;
62
              match graphFindCnstr cset with
63
              | Some (OpenC nodes) ->
64
                  let prop acc node =
65
                    match node with
66
                    | Core core -> (UCore (core, true))::acc
67
                    | State state -> (UState (state, None))::acc
68
                  in
69
                  List.fold_left prop tl nodes
70
              | _ -> assert false
71
            end else tl
72
      in
73
      propSat setStates setCores setCnstr tl1
74

    
75
let propagateSat () =
76
  let setStates = setEmptyState () in
77
  let setCores = setEmptyCore () in
78
  let setCnstr = setEmptyCnstr () in
79
  let fktS1 state =
80
    match stateGetStatus state with
81
    | Expandable
82
    | Open -> setAddState setStates state
83
    | Unsat
84
    | Sat -> ()
85
  in
86
  graphIterStates fktS1;
87
  let fktC1 core =
88
    match coreGetStatus core with
89
    | Expandable
90
    | Open -> setAddCore setCores core
91
    | Unsat
92
    | Sat -> ()
93
  in
94
  graphIterCores fktC1;
95
  let cfkt1 cset cnstr =
96
    if csetHasDot cset then ()
97
    else
98
      match cnstr with
99
      | OpenC _ -> setAddCnstr setCnstr cset
100
      | UnsatC
101
      | SatC
102
      | UnexpandedC _ -> ()
103
  in
104
  graphIterCnstrs cfkt1;
105
  graphIterStates (fun state -> propSat setStates setCores setCnstr [UState (state, None)]);
106
  graphIterCores (fun core -> propSat setStates setCores setCnstr [UCore (core, false)]);
107
  setIterState (fun state -> stateSetStatus state Sat) setStates;
108
  let setCoreSat core =
109
    coreSetStatus core Sat;
110
    if core == graphGetRoot () then raise (CoAlg_finished true) else ()
111
  in
112
  setIterCore setCoreSat setCores;
113
  setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
114

    
115

    
116
let propagateSatMu () =
117
  let setFinishingStates = setEmptyState () in
118
  let setFinishingCores = setEmptyCore () in
119
  let setStates = setEmptyState () in
120
  let setCores = setEmptyCore () in
121
  let emptySet = bsetMakeRealEmpty () in
122

    
123
  let stateCollector state =
124
    match stateGetStatus state with
125
    | Unsat -> ()
126
    | Sat ->
127
       setAddState setFinishingStates state
128
    | Expandable -> ()
129
    | Open ->
130
       if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
131
       then begin
132
         setAddState setFinishingStates state;
133
         stateSetStatus state Sat
134
       end else begin
135
         setAddState setStates state;
136
         if bsetCompare (stateGetDeferral state) emptySet == 0
137
         then begin
138
           print_endline (stateToString state);
139
           setAddState setFinishingStates state
140
         end
141
         else ()
142
       end
143
  in
144
  let coreCollector core =
145
    match coreGetStatus core with
146
    | Unsat -> ()
147
    | Sat ->
148
       setAddCore setFinishingCores core
149
    | Expandable
150
    | Open ->
151
       setAddCore setCores core;
152
       if bsetCompare (coreGetDeferral core) emptySet == 0
153
       then begin
154
           print_endline (coreToString core);
155
           setAddCore setFinishingCores core
156
         end
157
       else ()
158
  in
159
  graphIterStates stateCollector;
160
  graphIterCores coreCollector;
161

    
162
  (*
163
    In a fixpoint the set called setStates / setCores is narrowed down.
164

    
165
    In each step only those states and cores are retained in setStates
166
    / setCores which reach one of setFinishing{States,Cores} in
167
    finitely many steps. This new set of States / Cores is collected
168
    as allowed{States,Cores} during each fixpoint iteration.
169

    
170
    Only those finishing nodes are retained that have allowed or
171
    Successfull Children.
172
  *)
173

    
174
  let rec fixpointstep setStates setCores =
175
    let allowedStates = setEmptyState () in
176
    let allowedCores = setEmptyCore () in
177

    
178
    let rec visitParentStates (core : core) : unit =
179
      print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core)));
180
      if not (setMemCore allowedCores core)
181
      then begin
182
        setAddCore allowedCores core;
183
        print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core)));
184
        let verifyParent (state,_) =
185
          let rules = stateGetRules state in
186
          let ruleiter (dependencies, corelist) =
187
            List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
188
              corelist
189
          in
190
          if List.for_all ruleiter rules
191
          then visitParentCores state
192
          else print_endline ("Not considering state "^(string_of_int (stateGetIdx state)))
193
        in
194
        List.iter verifyParent (coreGetParents core)
195
      end
196

    
197
    and visitParentCores (state : state) : unit =
198
      print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state)));
199
      if not (setMemState allowedStates state)
200
      then begin
201
        setAddState allowedStates state;
202
        print_endline ("Adding State " ^ (string_of_int (stateGetIdx state)));
203
        let verifyParent core =
204
          let acceptable =
205
            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
206
              (coreGetChildren core)
207
          in
208
          if acceptable
209
          then visitParentStates core
210
          else print_endline ("Not considering state "^(string_of_int (coreGetIdx core)))
211
        in
212
        List.iter verifyParent (stateGetParents state)
213
      end
214
    in
215

    
216
    (* All rule applications need to still be potentially Sat for a
217
     * finishing State to be a valid startingpoint for this fixpoint.
218
     *)
219
    let checkFinishingState (state : state) =
220
      let ruleiter (dependencies, corelist) : bool =
221
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
222
      in
223
      if not (List.exists ruleiter (stateGetRules state)) then begin
224
        print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node");
225
        visitParentCores state
226
      end
227

    
228
    (* There needs to be a State still potentially Sat for this core
229
     * to be considered for the fixpoint
230
     *)
231
    and checkFinishingCore (core : core) =
232
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
233
                           (coreGetChildren core))
234
      then begin
235
        print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node");
236
        visitParentStates core
237
      end
238
    in
239
    setIterState checkFinishingState setFinishingStates;
240
    setIterCore checkFinishingCore setFinishingCores;
241

    
242

    
243
    if (setLengthState setStates) = (setLengthState allowedStates) &&
244
         (setLengthCore setCores) = (setLengthCore allowedCores)
245
    then begin
246
        setIterState (fun state -> stateSetStatus state Sat) setStates;
247
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
248
      end else
249
      fixpointstep allowedStates allowedCores
250
  in
251
  fixpointstep setStates setCores
252

    
253

    
254
(*****************************************************************************)
255
(*                     Propagation of Unsatisfiability                       *)
256
(*****************************************************************************)
257

    
258
let isConstraintUnsat cset =
259
  match graphFindCnstr cset with
260
  | None -> assert false
261
  | Some UnsatC -> true
262
  | _ -> false
263

    
264
let fhtMustFind fht f =
265
  match fhtFind fht f with
266
  | Some l -> l
267
  | None -> assert false
268

    
269
let lhtMustFind lht l =
270
  match lhtFind lht l with
271
  | Some f -> f
272
  | None -> assert false
273

    
274

    
275
(* Gets a list of Things we know are unsatisfiable and propagates this
276
   information backwards *)
277
let rec propagateUnsat = function
278
  | [] -> ()
279
  | propElem::tl ->
280
      let tl1 =
281
        match propElem with
282
        | UState (state, idxopt) -> begin
283
            match stateGetStatus state with
284
            | Unsat -> tl
285
            | Sat -> raise (ReasonerError ("Propagation tells state "
286
                                           ^(string_of_int (stateGetIdx state))
287
                                           ^" would be unsat, but it is already sat"))
288
            | Open
289
            | Expandable ->
290
                let mbs =
291
                  match idxopt with
292
                  | None -> stateGetBs state
293
                  | Some idx ->
294
                      let (dep, children) = stateGetRule state idx in
295
                      let getBs core =
296
                        assert (coreGetStatus core = Unsat);
297
                        coreGetBs core
298
                      in
299
                      dep (List.map getBs children)
300
                in
301
                stateSetBs state mbs;
302
                stateSetStatus state Unsat;
303
                let prop acc core =
304
                  let turnsUnsat =
305
                    match coreGetStatus core with
306
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
307
                    | Expandable
308
                    | Unsat
309
                    | Sat -> false
310
                  in
311
                  if turnsUnsat then (UCore (core, false))::acc else acc
312
                in
313
                List.fold_left prop tl (stateGetParents state)
314
          end
315
        | UCore (core, comesFromCnstr) -> begin
316
            match coreGetStatus core with
317
            | Unsat -> tl
318
            | Sat -> raise (ReasonerError ("Propagation tells core "
319
                                           ^(string_of_int (coreGetIdx core))
320
                                           ^" would be unsat, but it is already sat"))
321
            | Open
322
            | Expandable ->
323
                let mbs =
324
                  if comesFromCnstr then coreGetBs core
325
                  else
326
                    let bs = coreGetBs core in
327
                    let solver = coreGetSolver core in
328
                    let fht = coreGetFht core in
329
                    let lht = lhtInit () in
330
                    let addLits f acc =
331
                      let lit = fhtMustFind fht f in
332
                      lhtAdd lht lit f;
333
                      lit::acc
334
                    in
335
                    let litset = bsetFold addLits bs [] in
336
                    let addClauses state =
337
                      let cbs = stateGetBs state in
338
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
339
                      let okay = M.add_clause solver clause in
340
                      assert okay
341
                    in
342
                    List.iter addClauses (coreGetChildren core);
343
                    let isSat = M.invoke_solver solver litset in
344
                    assert (not isSat);
345
                    let res = bsetMake () in
346
                    let confls = M.get_conflict solver in
347
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
348
                    res
349
                in
350
                coreSetBs core mbs;
351
                coreSetStatus core Unsat;
352
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
353
                let prop acc (state, idx) =
354
                  let turnsUnsat =
355
                    match stateGetStatus state with
356
                    | Open
357
                    | Expandable ->
358
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
359
                    | Unsat
360
                    | Sat -> false
361
                  in
362
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
363
                in
364
                let tl2 = List.fold_left prop tl (coreGetParents core) in
365
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
366
          end
367
        | UCnstr cset ->
368
            match graphFindCnstr cset with
369
            | None
370
            | Some SatC -> assert false
371
            | Some UnsatC -> tl
372
            | Some (UnexpandedC nodes)
373
            | Some (OpenC nodes) ->
374
                graphReplaceCnstr cset UnsatC;
375
                let prop acc node =
376
                  match node with
377
                  | State state ->
378
                      let turnsUnsat =
379
                        match stateGetStatus state with
380
                        | Expandable
381
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
382
                        | Unsat
383
                        | Sat -> false
384
                      in
385
                      if turnsUnsat then (UState (state, None))::acc else acc
386
                  | Core core ->
387
                      let turnsUnsat =
388
                        match coreGetStatus core with
389
                        | Expandable
390
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
391
                        | Unsat
392
                        | Sat -> false
393
                      in
394
                      if turnsUnsat then (UCore (core, true))::acc else acc
395
                in
396
                List.fold_left prop tl nodes
397
      in
398
      propagateUnsat tl1
399

    
400

    
401
(*****************************************************************************)
402
(*                   Propagation of Nominal Constraints                      *)
403
(*****************************************************************************)
404

    
405
let extractAts sort bs =
406
  let ats = csetMake () in
407
  let procNom nom f =
408
    match lfGetType sort f with
409
    | AndF
410
    | OrF -> ()
411
    | TrueFalseF
412
    | AtF -> ()
413
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
414
  in
415
  let getAts f =
416
    match lfGetType sort f with
417
    | AtF -> csetAdd ats (lfToAt sort f)
418
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
419
    | _ -> ()
420
  in
421
  bsetIter getAts bs;
422
  ats
423

    
424
let detConstraintsState state =
425
  let procRule accR (_, chldrn) =
426
    let procChldrn accC core =
427
      if coreGetStatus core = Unsat then accC
428
      else cssUnion accC (coreGetConstraints core)
429
    in
430
    let orset = List.fold_left procChldrn cssEmpty chldrn in
431
    let procOrset csetO accO =
432
      let mkUnion csetU accU =
433
        let cset = csetUnion csetO csetU in
434
        cssAdd cset accU
435
      in
436
      cssFold mkUnion accR accO
437
    in
438
    cssFold procOrset orset cssEmpty
439
  in
440
  let sort = stateGetSort state in
441
  let bs = stateGetBs state in
442
  let ats = extractAts sort bs in
443
  if stateGetStatus state = Expandable then csetAddDot ats else ();
444
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
445

    
446
let detConstraintsCore core =
447
  let sort = coreGetSort core in
448
  let bs = coreGetBs core in
449
  let ats = extractAts sort bs in
450
  let addCnstr acc state =
451
    if stateGetStatus state = Unsat then acc
452
    else
453
      let csets = stateGetConstraints state in
454
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
455
      cssUnion csets acc
456
  in
457
  let initInner =
458
    if coreGetStatus core = Expandable then
459
      (* let cset = csetCopy ats in *)
460
      let cset = ats in
461
      csetAddDot cset;
462
      cssSingleton cset
463
    else cssEmpty
464
  in
465
  List.fold_left addCnstr initInner (coreGetChildren core)
466

    
467
let rec propNom = function
468
  | [] -> ()
469
  | node::tl ->
470
      let tl1 =
471
        match node with
472
        | State state ->
473
            if stateGetStatus state = Unsat then tl
474
            else
475
              let csets = detConstraintsState state in
476
              let oldcsets = stateGetConstraints state in
477
              if cssEqual csets oldcsets then tl
478
              else begin
479
                stateSetConstraints state csets;
480
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
481
              end
482
        | Core core ->
483
            if coreGetStatus core = Unsat then tl
484
            else
485
              let csets = detConstraintsCore core in
486
              let oldcsets = coreGetConstraints core in
487
              if cssEqual csets oldcsets then tl
488
              else begin
489
                coreSetConstraints core csets;
490
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
491
              end
492
      in
493
      propNom tl1
494

    
495
let updateConstraints node elemU csets =
496
  let update cset acc =
497
    let cnstr =
498
      match graphFindCnstr cset with
499
      | Some cn -> cn
500
      | None ->
501
          let cn = UnexpandedC [] in
502
          graphInsertCnstr cset cn;
503
          queueInsertCnstr cset;
504
          cn
505
    in
506
    match cnstr with
507
    | UnsatC -> acc
508
    | UnexpandedC parents ->
509
        graphReplaceCnstr cset (UnexpandedC (node::parents));
510
        false
511
    | OpenC parents ->
512
        graphReplaceCnstr cset (OpenC (node::parents));
513
        false
514
    | SatC -> false
515
  in
516
  let isUnsat = cssFold update csets true in
517
  if isUnsat then propagateUnsat [elemU] else ()
518

    
519
let propagateNominals () =
520
  let init = cssSingleton (csetMake ()) in
521
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
522
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
523
  graphIterStates (fun s -> propNom [State s]);
524
  graphIterCores (fun c -> propNom [Core c]);
525
  graphClearCnstr ();
526
  let fktS state =
527
    if stateGetStatus state = Unsat then ()
528
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
529
  in
530
  graphIterStates fktS;
531
  let fktC core =
532
    if coreGetStatus core = Unsat then ()
533
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
534
  in
535
  graphIterCores fktC
536

    
537

    
538
(*****************************************************************************)
539
(*                           Node Expansions                                 *)
540
(*****************************************************************************)
541

    
542
let getLit sort fht solver f =
543
  match fhtFind fht f with
544
  | Some lit -> lit
545
  | None ->
546
      let var = M.new_variable solver in
547
      let lit = M.var_to_lit var true in
548
      fhtAdd fht f lit;
549
      let () =
550
        match lfGetNeg sort f with
551
        | None -> ()
552
        | Some nf ->
553
            let nlit = M.neg_lit lit in
554
            fhtAdd fht nf nlit;
555
      in
556
      lit
557

    
558
let newCore sort bs defer =
559
  (* when creating a now core from a set of formulas bs
560
        bs = { x_1, ...., x_n }
561
           = "x_1 /\ .... /\ x_n"
562
     Then we do this by:
563

    
564
        1. creating a new literal in the sat solver for each
565
           "boolean subformula" from the x_i. "boolean subformula" means that
566
           this subformula is not hidden under modalities but only under
567
           boolean connectives (/\, \/).
568
        2. encoding the relation between a formula and its intermediate boolean
569
           subformulas by a clause:
570
  *)
571
  let fht = fhtInit () in
572
  let solver = M.new_solver () in
573
  let rec addClauses f =
574
    (* step 1: create a literal in the satsolver representing the formula f *)
575
    let lf = getLit sort fht solver f in
576
    (* step 2: encode relation to possible subformulas *)
577
    match lfGetType sort f with
578
    | OrF ->
579
        (*
580
           case 2.(a)   f =  f1 \/ f2
581
                   fill fht such that it says:
582

    
583
                        f  |---> lf
584
                        f1 |---> lf1
585
                        f2 |---> lf2
586
        *)
587
        let f1 = lfGetDest1 sort f in
588
        let f2 = lfGetDest2 sort f in
589
        addClauses f1;
590
        addClauses f2;
591
        let lf1 = fhtMustFind fht f1 in
592
        let lf2 = fhtMustFind fht f2 in
593
        (*
594
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
595
        *)
596
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
597
        assert (okay)
598
    | AndF ->
599
        (*
600
           case 2.(b)   f =  f1 /\ f2
601
                   fill fht such that it says:
602

    
603
                        f  |---> lf
604
                        f1 |---> lf1
605
                        f2 |---> lf2
606
        *)
607
        let f1 = lfGetDest1 sort f in
608
        let f2 = lfGetDest2 sort f in
609
        addClauses f1;
610
        addClauses f2;
611
        let lf1 = fhtMustFind fht f1 in
612
        let lf2 = fhtMustFind fht f2 in
613
        (*
614
            encode the structure of f by adding the clauses
615
                    (lf -> lf1) /\ (lf -> lf2)
616
        *)
617
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
618
        assert (okay1);
619
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
620
        assert (okay2)
621
    | MuF
622
    | NuF ->
623
       (*
624
          Dest of a fixpoint is it's unfolded version. This adds just
625
          an simple forward implication that could be optimised out
626
          though not without nontrivial transformation of code
627

    
628
            f = μ X . φ   |---> lf
629
            φ[X |-> f]    |---> lf1
630

    
631
          Then adding lf -> lf1 to minisat
632
        *)
633
       let f1 = lfGetDest1 sort f in
634
       addClauses f1;
635
       let lf1 = fhtMustFind fht f1 in
636
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
637
       assert (okay1);
638
    | _ -> ()
639
        (* case 2.(c)
640
            We don't need to do anything except adding f to the fht
641
        *)
642
  in
643
  bsetIter addClauses bs;
644
  coreMake sort bs defer solver fht
645

    
646
let getNextState core =
647
  (* Create a new state, which is obtained by a satisfying assignment of the
648
     literals of the minisat solver.
649
     In addition to that, feed the negation of the satisfying assignment back
650
     to the minisat solver in order to obtain different solutions on successive
651
     minisat calls.
652
  *)
653
  let bs = coreGetBs core in
654
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
655
  let deferralS =
656
    if refocusing then
657
      bsetCopy bs
658
    else
659
      coreGetDeferral core
660
  in
661
  let fht = coreGetFht core in
662
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
663
  let solver = coreGetSolver core in
664
  let isSat = M.invoke_solver solver litset in
665
  (* Clearly, if the current core is unsatisfiable, no further child state can
666
     be created *)
667
  if not isSat then None
668
  else
669
    let sort = coreGetSort core in
670
    (* create a new set of formulas newbs with the property:
671
       if the conjunction of newbs is satisfiable, then the present core is
672
       satisfiable.
673
    *)
674
    let newbs = bsetMake () in
675
    let newdefer = bsetMakeRealEmpty () in
676
    (* if newbs = { l_1, .... l_n }, i.e.
677

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

    
680
       then we can get essentially different satisfying assignments of bs by
681
       adding another clause
682

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

    
685
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
686
    *)
687
    let rec mkExclClause deferral f acc =
688
      (* f is a formula that is true in the current satisfying assignment *)
689
      match lfGetType sort f with
690
      | OrF ->
691
          (* if f is true and a disjunction, then one of its disjuncts is true *)
692
          let f1 = lfGetDest1 sort f in
693
          let lf1 = fhtMustFind fht f1 in
694
          (* if the first disjunct f1 is true, then we need to add subformulas
695
             of f1 to newbs&clause *)
696
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
697
          else
698
            (* otherwise f2 must be true *)
699
            let f2 = lfGetDest2 sort f in
700
            let lf2 = fhtMustFind fht f2 in
701
            assert (M.literal_status solver lf2 = M.LTRUE);
702
            mkExclClause deferral f2 acc
703
      | AndF ->
704
          (* if the true f is a conjuction, then both conjunctions must be true *)
705
          let f1 = lfGetDest1 sort f in
706
          let lf1 = fhtMustFind fht f1 in
707
          assert (M.literal_status solver lf1 = M.LTRUE);
708
          let acc1 = mkExclClause deferral f1 acc in
709
          let f2 = lfGetDest2 sort f in
710
          let lf2 = fhtMustFind fht f2 in
711
          assert (M.literal_status solver lf2 = M.LTRUE);
712
          mkExclClause deferral f2 acc1
713
      | MuF
714
      | NuF ->
715
         let f1 = lfGetDest1 sort f in
716
         mkExclClause deferral f1 acc
717
      | _ ->
718
         (* if f is a trivial formula or modality, then add it ... *)
719
         (* ... to newbs *)
720
         bsetAdd newbs f;
721
         let defercandidate = lfGetDeferral sort f in
722
         (if (defercandidate != (Hashtbl.hash "ε") &&
723
                (refocusing || deferral = defercandidate)) then
724
            bsetAdd newdefer f);
725
         (* ... and to the new clause *)
726
         (M.neg_lit (fhtMustFind fht f))::acc
727
    in
728
    let init_clause f acc =
729
      let deferral =
730
        if bsetMem deferralS f then (
731
          lfGetDeferral sort f)
732
        else
733
          (Hashtbl.hash "ε")
734
      in
735
      mkExclClause deferral f acc
736
    in
737
    let clause = bsetFold init_clause bs [] in
738
    let okay = M.add_clause solver clause in
739
    assert (okay);
740
    Some (sort, newbs, newdefer)
741

    
742
let newState sort bs defer =
743
  let (func, sl) = !sortTable.(sort) in
744
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
745
  let exp = producer sort bs defer sl in
746
  stateMake sort bs defer exp
747

    
748
let insertState parent sort bs defer =
749
  let child =
750
    match graphFindState sort (bs, defer) with
751
    | None ->
752
        let s = newState sort bs defer in
753
        graphInsertState sort (bs, defer) s;
754
        queueInsertState s;
755
        s
756
    | Some s -> s
757
  in
758
  coreAddChild parent child;
759
  stateAddParent child parent
760

    
761
let expandCore core =
762
  match getNextState core with
763
  | Some (sort, bs, defer) ->
764
      insertState core sort bs defer;
765
      queueInsertCore core
766
  | None ->
767
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
768
      if isUnsat then propagateUnsat [UCore (core, false)]
769
      else coreSetStatus core Open
770

    
771

    
772
let insertCore sort bs defer =
773
  match graphFindCore sort (bs, defer) with
774
  | None ->
775
     let c = newCore sort bs defer in
776
     graphInsertCore sort (bs, defer) c;
777
     queueInsertCore c;
778
     c
779
  | Some c -> c
780

    
781
let insertRule state dep chldrn =
782
  let chldrn = listFromLazylist chldrn in
783
  let insert (isUns, acc) (sort, bs, defer) =
784
    let bs1 = bsetAddTBox sort bs in
785
    let core = insertCore sort bs1 defer in
786
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
787
    (isUns1, core::acc)
788
  in
789
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
790
  let idx = stateAddRule state dep (List.rev children) in
791
  List.iter (fun c -> coreAddParent c state idx) children;
792
  if isUnsat then begin
793
    propagateUnsat [UState (state, Some idx)];
794
    false
795
  end else true
796

    
797
let rec insertAllRules state = function
798
  | [] -> true
799
  | (dep, chldrn)::tl ->
800
      let notUnsat = insertRule state dep chldrn in
801
      if notUnsat then insertAllRules state tl else false
802

    
803
let expandState state =
804
  match stateNextRule state with
805
  | MultipleElements rules ->
806
      let notUnsat = insertAllRules state rules in
807
      if notUnsat then stateSetStatus state Open
808
  | SingleElement (dep, chldrn) ->
809
      let notUnsat = insertRule state dep chldrn in
810
      if notUnsat then queueInsertState state else ()
811
  | NoMoreElements -> stateSetStatus state Open
812

    
813

    
814
let expandCnstr cset =
815
  let nht = nhtInit () in
816
  let mkCores f =
817
    let (sort, lf) as nom = atFormulaGetNominal f in
818
    let nomset =
819
      match nhtFind nht nom with
820
      | Some ns -> ns
821
      | None ->
822
          let cset1 = csetCopy cset in
823
          csetRemDot cset1;
824
          let bs = csetAddTBox sort cset1 in
825
          bsetAdd bs lf;
826
          nhtAdd nht nom bs;
827
          bs
828
    in
829
    bsetAdd nomset (atFormulaGetSubformula f)
830
  in
831
  csetIter cset mkCores;
832
  let inCores (sort, _) bs (isUns, acc) =
833
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
834
    coreAddConstraintParent core cset;
835
    (coreGetStatus core = Unsat || isUns, core::acc)
836
  in
837
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
838
  if isUnsat then propagateUnsat [UCnstr cset]
839
  else
840
    match graphFindCnstr cset with
841
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
842
    | _ -> assert false
843

    
844

    
845
(*****************************************************************************)
846
(*                           The Main Loop                                   *)
847
(*****************************************************************************)
848

    
849
let expandNodesLoop (recursiveAction: unit -> unit) =
850
  match queueGetElement () with
851
  | QState state ->
852
      if stateGetStatus state = Expandable then begin
853
        expandState state;
854
        if doNominalPropagation () then begin
855
          propagateNominals ();
856
          if doSatPropagation () then propagateSatMu ()
857
        end else ()
858
      end else ();
859
      recursiveAction ()
860
  | QCore core ->
861
      if coreGetStatus core = Expandable then begin
862
        expandCore core;
863
        if doNominalPropagation () then begin
864
          propagateNominals ();
865
          if doSatPropagation () then propagateSatMu ()
866
        end else ()
867
      end else ();
868
      recursiveAction ()
869
  | QCnstr cset ->
870
      expandCnstr cset;
871
      recursiveAction ()
872
  | QEmpty -> ()
873

    
874
let runReasonerStep () =
875
  let void () = () in
876
  expandNodesLoop void; (* expand at most one node *)
877
  (* if this emptied the queue *)
878
  if queueIsEmpty () then begin
879
    (* then check whether the nominals would add further queue elements *)
880
    print_endline "Propagating nominals...";
881
    propagateNominals ()
882
  end else () (* else: the next step would be to expand another node *)
883

    
884
let rec buildGraphLoop () =
885
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
886
  expandNodesFurther (); (* expand as many queue elements as possible *)
887
  propagateNominals ();
888
  (* if propagating nominals added some more queue members, do all again.. *)
889
  if queueIsEmpty () then () else buildGraphLoop ()
890

    
891
let initReasoner sorts nomTable tbox sf =
892
  sortTable := Array.copy sorts;
893
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
894
  let sort = fst sf in
895
  let bs1 = bsetAddTBox sort bs in
896
  let deferrals = bsetMakeRealEmpty() in
897
  let markDeferral f =
898
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
899
      bsetAdd deferrals f;)
900
  in
901
  bsetIter markDeferral bs;
902
  graphInit ();
903
  queueInit ();
904
  let root = insertCore sort bs1 deferrals in
905
  graphAddRoot root
906

    
907
let isRootSat () =
908
  match coreGetStatus (graphGetRoot ()) with
909
  | Expandable -> None
910
  | Unsat -> Some false
911
  | Sat -> if (queueIsEmpty()) then Some true else None
912
  | Open -> if (queueIsEmpty()) then Some false else None
913

    
914
let reasonerFinished () =
915
  match coreGetStatus (graphGetRoot ()) with
916
  | Expandable -> false
917
  | Unsat
918
  | Sat  -> true
919
  | Open -> queueIsEmpty ()
920

    
921

    
922
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
923
    @param verbose An optional switch which determines
924
    whether the procedure shall print some information on the standard output.
925
    The default is false.
926
    @param sorts An array mapping each sort (represented as an integer)
927
    to a functor and a list of sorts which are the arguments of the functor.
928
    @param nomTable A partial function mapping nominals (represented as strings)
929
    to their sorts.
930
    @param tbox A list of sorted formulae.
931
    @param sf A sorted formula.
932
    @return True if sf is satisfiable wrt tbox, false otherwise.
933
 *)
934

    
935
let isSat ?(verbose = false) sorts nomTable tbox sf =
936
  let start = if verbose then Unix.gettimeofday () else 0. in
937
  initReasoner sorts nomTable tbox sf;
938
  let sat =
939
    try
940
      buildGraphLoop ();
941
      (* get whether the root is satisfiable *)
942
      (* we know that the reasoner finished, so the value is there, *)
943
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
944
      CU.fromSome (isRootSat())
945
    with CoAlg_finished res -> res
946
  in
947
  (* print some statistics *)
948
  if verbose then
949
    let stop = Unix.gettimeofday () in
950
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
951
    print_newline ();
952
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
953
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
954
    print_endline ("Added Size: " ^ (string_of_int size));
955
    (*
956
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
957
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
958
    print_endline ("Added Size: " ^ (string_of_int nsize));
959
    *)
960
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
961
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
962
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
963
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
964
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
965
    print_newline ()
966
  else ();
967
  sat