Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 07a36b24

History | View | Annotate | Download (32.9 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 setSatStates = setEmptyState () in
122
  let setSatCores = setEmptyCore () in
123
  let emptySet = bsetMakeRealEmpty () in
124

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

    
158
  (*
159
    In a fixpoint the set called setStates / setCores is narrowed down.
160

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

    
166
    Only those finishing nodes are retained that have allowed or
167
    Successfull Children.
168
  *)
169

    
170
  let rec fixpointstep setStates setCores =
171
    let allowedStates = setEmptyState () in
172
    let allowedCores = setEmptyCore () in
173

    
174
    let rec visitParentStates (core : core) : unit =
175
      if not (setMemCore setCores core) then ()
176
      else begin
177
        let children = coreGetChildren core in
178
        let acceptable =
179
          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
180
            children
181
        in
182
        if acceptable then begin
183
          print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
184
          setAddCore allowedCores core;
185
          List.iter (fun (state, _) -> visitParentCores state)
186
            (coreGetParents core)
187
        end
188
      end
189

    
190
    and visitParentCores (state : state) : unit =
191
      if not (setMemState setStates state) then ()
192
      else begin
193
        let rules = stateGetRules state in
194
        let ruleiter (dependencies, corelist) =
195
          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
196
            corelist
197
        in
198
        let acceptable = List.for_all ruleiter rules in
199
        if acceptable then begin
200
          print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
201
          setAddState allowedStates state;
202
          List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core)
203
            (stateGetParents state)
204
        end
205
      end
206
    in
207

    
208
    (* All rule applications need to still be potentially Sat for a
209
     * finishing State to be a valid startingpoint for this fixpoint.
210
     *)
211
    let checkFinishingState (state : state) =
212
      let ruleiter (dependencies, corelist) : bool =
213
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
214
      in
215
      if not (List.exists ruleiter (stateGetRules state)) then begin
216
        setAddState allowedStates state;
217
        visitParentCores state
218
      end
219

    
220
    (* There needs to be a State still potentially Sat for this core
221
     * to be considered for the fixpoint
222
     *)
223
    and checkFinishingCore (core : core) =
224
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
225
                           (coreGetChildren core))
226
      then begin
227
        setAddCore allowedCores core;
228
        visitParentStates core
229
      end
230
    in
231
    setIterState checkFinishingState setFinishingStates;
232
    setIterCore checkFinishingCore setFinishingCores;
233
    setIterState visitParentCores setSatStates;
234
    setIterCore visitParentStates setSatCores;
235

    
236

    
237
    if (setLengthState setStates) = (setLengthState allowedStates) &&
238
         (setLengthCore setCores) = (setLengthCore allowedCores)
239
    then begin
240
        setIterState (fun state -> stateSetStatus state Sat) setStates;
241
        setIterCore (fun core -> coreSetStatus core Sat) setCores;
242
      end else
243
      fixpointstep allowedStates allowedCores
244
  in
245
  fixpointstep setStates setCores
246

    
247

    
248
(*****************************************************************************)
249
(*                     Propagation of Unsatisfiability                       *)
250
(*****************************************************************************)
251

    
252
let isConstraintUnsat cset =
253
  match graphFindCnstr cset with
254
  | None -> assert false
255
  | Some UnsatC -> true
256
  | _ -> false
257

    
258
let fhtMustFind fht f =
259
  match fhtFind fht f with
260
  | Some l -> l
261
  | None -> assert false
262

    
263
let lhtMustFind lht l =
264
  match lhtFind lht l with
265
  | Some f -> f
266
  | None -> assert false
267

    
268

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

    
394

    
395
(*****************************************************************************)
396
(*                   Propagation of Nominal Constraints                      *)
397
(*****************************************************************************)
398

    
399
let extractAts sort bs =
400
  let ats = csetMake () in
401
  let procNom nom f =
402
    match lfGetType sort f with
403
    | AndF
404
    | OrF -> ()
405
    | TrueFalseF
406
    | AtF -> ()
407
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
408
  in
409
  let getAts f =
410
    match lfGetType sort f with
411
    | AtF -> csetAdd ats (lfToAt sort f)
412
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
413
    | _ -> ()
414
  in
415
  bsetIter getAts bs;
416
  ats
417

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

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

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

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

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

    
531

    
532
(*****************************************************************************)
533
(*                           Node Expansions                                 *)
534
(*****************************************************************************)
535

    
536
let getLit sort fht solver f =
537
  match fhtFind fht f with
538
  | Some lit -> lit
539
  | None ->
540
      let var = M.new_variable solver in
541
      let lit = M.var_to_lit var true in
542
      fhtAdd fht f lit;
543
      let () =
544
        match lfGetNeg sort f with
545
        | None -> ()
546
        | Some nf ->
547
            let nlit = M.neg_lit lit in
548
            fhtAdd fht nf nlit;
549
      in
550
      lit
551

    
552
let newCore sort bs defer =
553
  (* when creating a now core from a set of formulas bs
554
        bs = { x_1, ...., x_n }
555
           = "x_1 /\ .... /\ x_n"
556
     Then we do this by:
557

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

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

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

    
622
            f = μ X . φ   |---> lf
623
            φ[X |-> f]    |---> lf1
624

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

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

    
672
            newbs = l_1 /\ ... /\ l_n
673

    
674
       then we can get essentially different satisfying assignments of bs by
675
       adding another clause
676

    
677
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
678

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

    
736
let newState sort bs defer =
737
  let (func, sl) = !sortTable.(sort) in
738
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
739
  let exp = producer sort bs defer sl in
740
  stateMake sort bs defer exp
741

    
742
let insertState parent sort bs defer =
743
  let child =
744
    match graphFindState sort (bs, defer) with
745
    | None ->
746
        let s = newState sort bs defer in
747
        graphInsertState sort (bs, defer) s;
748
        queueInsertState s;
749
        s
750
    | Some s -> s
751
  in
752
  coreAddChild parent child;
753
  stateAddParent child parent
754

    
755
let expandCore core =
756
  match getNextState core with
757
  | Some (sort, bs, defer) ->
758
      insertState core sort bs defer;
759
      queueInsertCore core
760
  | None ->
761
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
762
      if isUnsat then propagateUnsat [UCore (core, false)]
763
      else coreSetStatus core Open
764

    
765

    
766
let insertCore sort bs defer =
767
  match graphFindCore sort (bs, defer) with
768
  | None ->
769
     let c = newCore sort bs defer in
770
     graphInsertCore sort (bs, defer) c;
771
     queueInsertCore c;
772
     c
773
  | Some c -> c
774

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

    
791
let rec insertAllRules state = function
792
  | [] -> true
793
  | (dep, chldrn)::tl ->
794
      let notUnsat = insertRule state dep chldrn in
795
      if notUnsat then insertAllRules state tl else false
796

    
797
let expandState state =
798
  match stateNextRule state with
799
  | MultipleElements rules ->
800
      let notUnsat = insertAllRules state rules in
801
      if notUnsat then stateSetStatus state Open
802
  | SingleElement (dep, chldrn) ->
803
      let notUnsat = insertRule state dep chldrn in
804
      if notUnsat then queueInsertState state else ()
805
  | NoMoreElements -> stateSetStatus state Open
806

    
807

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

    
838

    
839
(*****************************************************************************)
840
(*                           The Main Loop                                   *)
841
(*****************************************************************************)
842

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

    
868
let runReasonerStep () =
869
  let void () = () in
870
  expandNodesLoop void; (* expand at most one node *)
871
  (* if this emptied the queue *)
872
  if queueIsEmpty () then begin
873
    (* then check whether the nominals would add further queue elements *)
874
    print_endline "Propagating nominals...";
875
    propagateNominals ()
876
  end else () (* else: the next step would be to expand another node *)
877

    
878
let rec buildGraphLoop () =
879
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
880
  expandNodesFurther (); (* expand as many queue elements as possible *)
881
  propagateNominals ();
882
  (* if propagating nominals added some more queue members, do all again.. *)
883
  if queueIsEmpty () then () else buildGraphLoop ()
884

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

    
901
let isRootSat () =
902
  match coreGetStatus (graphGetRoot ()) with
903
  | Expandable -> None
904
  | Unsat -> Some false
905
  | Sat
906
  | Open -> if (queueIsEmpty()) then Some true else None
907

    
908
let reasonerFinished () =
909
  match coreGetStatus (graphGetRoot ()) with
910
  | Expandable -> false
911
  | Unsat
912
  | Sat  -> true
913
  | Open -> queueIsEmpty ()
914

    
915

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

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