Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ e1489b0d

History | View | Annotate | Download (38.8 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
  (* Collect two sets of nodes. All nodes that may be satisfiable
124
   * after this iteration are collected into setStates/setCores.
125
   *
126
   * As every cycle containing a node with empty focus or an
127
   * satisfiable node should be considered satisfiable, collect these
128
   * decisive nodes into setFinishingStates/setFinishingCores
129
   *
130
   * This also marks in trivial cases nodes as satisfiable.
131
   *)
132
  let stateCollector state =
133
    match stateGetStatus state with
134
    | Unsat -> ()
135
    | Sat ->
136
       setAddState setStates state;
137
      setAddState setFinishingStates state
138
    | Expandable -> ()
139
    | Open ->
140
       if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
141
         bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
142
       then begin
143
         setAddState setFinishingStates state;
144
         stateSetStatus state Sat
145
       end else begin
146
         setAddState setStates state;
147
         if bsetCompare (stateGetDeferral state) emptySet == 0
148
         then begin
149
           print_endline (stateToString state);
150
           setAddState setFinishingStates state
151
         end
152
         else ()
153
       end
154

    
155
  (* As it is enough for a core to have one successfull child, we can
156
   * also handle (some) expandable cores.
157
   *)
158
  and coreCollector core =
159
    match coreGetStatus core with
160
    | Unsat -> ()
161
    | Sat ->
162
       setAddCore setCores core;
163
       setAddCore setFinishingCores core
164
    | Expandable
165
    | Open ->
166
       setAddCore setCores core;
167
      if bsetCompare (coreGetDeferral core) emptySet == 0
168
      then begin
169
        print_endline (coreToString core);
170
        setAddCore setFinishingCores core
171
      end
172
      else ()
173
  in
174
  graphIterStates stateCollector;
175
  graphIterCores coreCollector;
176

    
177
  (* In a fixpoint the set called setStates / setCores is narrowed
178
   * down.
179
   *
180
   * In each step only those states and cores are retained in setStates
181
   * / setCores which reach one of setFinishing{States,Cores} in
182
   * finitely many steps. This new set of States / Cores is collected
183
   * as allowed{States,Cores} during each fixpoint iteration.
184
   *
185
   * Only those finishing nodes are retained that have allowed or
186
   * Successfull Children.
187
   *)
188
  let rec fixpointstep setStates setCores =
189
    let allowedStates = setEmptyState () in
190
    let allowedCores = setEmptyCore () in
191

    
192
    let rec visitParentStates (core : core) : unit =
193
      print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core)));
194
      if not (setMemCore allowedCores core)
195
      then begin
196
        setAddCore allowedCores core;
197
        print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core)));
198
        let verifyParent (state,_) =
199
          let rules = stateGetRules state in
200
          let ruleiter (dependencies, corelist) =
201
            List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
202
              corelist
203
          in
204
          if List.for_all ruleiter rules
205
          then visitParentCores state
206
          else print_endline ("Not considering state "^(string_of_int (stateGetIdx state)))
207
        in
208
        List.iter verifyParent (coreGetParents core)
209
      end
210

    
211
    and visitParentCores (state : state) : unit =
212
      print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state)));
213
      if not (setMemState allowedStates state)
214
      then begin
215
        setAddState allowedStates state;
216
        print_endline ("Adding State " ^ (string_of_int (stateGetIdx state)));
217
        let verifyParent core =
218
          let acceptable =
219
            List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
220
              (coreGetChildren core)
221
          in
222
          if acceptable
223
          then visitParentStates core
224
          else print_endline ("Not considering state "^(string_of_int (coreGetIdx core)))
225
        in
226
        List.iter verifyParent (stateGetParents state)
227
      end
228
    in
229

    
230
    (* All rule applications need to still be potentially Sat for a
231
     * finishing State to be a valid startingpoint for this fixpoint.
232
     *)
233
    let checkFinishingState (state : state) =
234
      let ruleiter (dependencies, corelist) : bool =
235
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
236
      in
237
      if not (List.exists ruleiter (stateGetRules state)) then begin
238
        print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node");
239
        visitParentCores state
240
      end
241

    
242
    (* There needs to be a State still potentially Sat for this core
243
     * to be considered for the fixpoint
244
     *)
245
    and checkFinishingCore (core : core) =
246
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
247
                           (coreGetChildren core))
248
      then begin
249
        print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node");
250
        visitParentStates core
251
      end
252
    in
253
    setIterState checkFinishingState setFinishingStates;
254
    setIterCore checkFinishingCore setFinishingCores;
255

    
256

    
257
    if (setLengthState setStates) = (setLengthState allowedStates) &&
258
         (setLengthCore setCores) = (setLengthCore allowedCores)
259
    then begin
260
        setIterState (fun state -> stateSetStatus state Sat) setStates;
261
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
262
      end else
263
      fixpointstep allowedStates allowedCores
264
  in
265
  fixpointstep setStates setCores
266

    
267

    
268
(*****************************************************************************)
269
(*                     Propagation of Unsatisfiability                       *)
270
(*****************************************************************************)
271

    
272
let isConstraintUnsat cset =
273
  match graphFindCnstr cset with
274
  | None -> assert false
275
  | Some UnsatC -> true
276
  | _ -> false
277

    
278
let fhtMustFind fht f =
279
  match fhtFind fht f with
280
  | Some l -> l
281
  | None -> assert false
282

    
283
let lhtMustFind lht l =
284
  match lhtFind lht l with
285
  | Some f -> f
286
  | None -> assert false
287

    
288

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

    
414
let propateUnsatMu () =
415
  let setFinishingStates = setEmptyState () in
416
  let setFinishingCores = setEmptyCore () in
417
  let setStates = setEmptyState () in
418
  let setCores = setEmptyCore () in
419
  let emptySet = bsetMakeRealEmpty () in
420

    
421
  (* Collect two sets of nodes. All nodes that may be unsatisfiable
422
   * after this iteration are collected into setStates/setCores.
423
   *
424
   * Nodes reaching Points with empty focus as well as Expandable nodes
425
   * (if not Unsat) can not be declared Unsat so we collect these into
426
   * setFinishingStates/setFinishingCores.
427
   *)
428
  let stateCollector state =
429
    match stateGetStatus state with
430
    | Unsat -> ()
431
    | Sat
432
    | Expandable ->
433
       setAddState setStates state;
434
      setAddState setFinishingStates state
435
    | Open ->
436
       setAddState setStates state;
437
      if bsetCompare (stateGetDeferral state) emptySet == 0
438
      then begin
439
        setAddState setFinishingStates state
440
      end
441
      else ()
442

    
443
  and coreCollector core =
444
    match coreGetStatus core with
445
    | Unsat -> ()
446
    | Expandable
447
    | Sat ->
448
       setAddCore setCores core;
449
      setAddCore setFinishingCores core
450
    | Open ->
451
       setAddCore setCores core;
452
      if bsetCompare (coreGetDeferral core) emptySet == 0
453
      then begin
454
        setAddCore setFinishingCores core
455
      end
456
      else ()
457
  in
458
  graphIterStates stateCollector;
459
  graphIterCores coreCollector;
460

    
461
  (* In a fixpoint the set called setFinishingStates/setFinishingCores
462
   * is narrowed down
463
   *
464
   * In each iteration we start with all Nodes and remove all that can
465
   * reach a finishing Node. We then remove all finishing Nodes from the
466
   * respective set which are becoming Unsat and start with the next
467
   * iteration until the fixpoint is reached
468
   *
469
   *
470
   *)
471
  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
472
    let setUnsatStates = setCopyState setStates in
473
    let setUnsatCores = setCopyCore setCores in
474

    
475
    let rec visitParentStates (core : core) : unit =
476
      if setMemCore setUnsatCores core
477
      then begin
478
        setRemoveCore setUnsatCores core;
479
        let verifyParent (state,_) =
480
          let rules = stateGetRules state in
481
          let ruleiter (dependencies, corelist) =
482
            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat)
483
              corelist
484
          in
485
          if List.for_all ruleiter rules
486
          then visitParentCores state
487
        in
488
        List.iter verifyParent (coreGetParents core)
489
      end
490

    
491
    and visitParentCores (state : state) : unit =
492
      if setMemState setUnsatStates state
493
      then begin
494
        setRemoveState setUnsatStates state;
495
        let verifyParent core =
496
          let acceptable =
497
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat)
498
              (coreGetChildren core)
499
          in
500
          if acceptable
501
          then visitParentStates core
502
        in
503
        List.iter verifyParent (stateGetParents state)
504
      end
505
    in
506

    
507
    (* All rule applications need to still be potentially Sat for a
508
     * finishing State to be a valid startingpoint for this fixpoint.
509
     *)
510
    let checkFinishingState (state : state) =
511
      let ruleiter (dependencies, corelist) : bool =
512
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist
513
      in
514
      if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin
515
        visitParentCores state
516
      end
517

    
518
    (* There needs to be a State still potentially Sat for this core
519
     * to be considered for the fixpoint
520
     *)
521
    and checkFinishingCore (core : core) =
522
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
523
                (coreGetChildren core)) ||
524
        coreGetStatus core == Expandable
525
      then begin
526
        visitParentStates core
527
      end
528
    in
529
    setIterState checkFinishingState setFinishingStates;
530
    setIterCore checkFinishingCore setFinishingCores;
531

    
532
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
533
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
534
    then begin
535
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
536
        setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores;
537
      end else
538
      fixpointstep setUnsatStates setUnsatCores
539
  in
540
  fixpointstep (setEmptyState ()) (setEmptyCore ())
541

    
542

    
543
(*****************************************************************************)
544
(*                   Propagation of Nominal Constraints                      *)
545
(*****************************************************************************)
546

    
547
let extractAts sort bs =
548
  let ats = csetMake () in
549
  let procNom nom f =
550
    match lfGetType sort f with
551
    | AndF
552
    | OrF -> ()
553
    | TrueFalseF
554
    | AtF -> ()
555
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
556
  in
557
  let getAts f =
558
    match lfGetType sort f with
559
    | AtF -> csetAdd ats (lfToAt sort f)
560
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
561
    | _ -> ()
562
  in
563
  bsetIter getAts bs;
564
  ats
565

    
566
let detConstraintsState state =
567
  let procRule accR (_, chldrn) =
568
    let procChldrn accC core =
569
      if coreGetStatus core = Unsat then accC
570
      else cssUnion accC (coreGetConstraints core)
571
    in
572
    let orset = List.fold_left procChldrn cssEmpty chldrn in
573
    let procOrset csetO accO =
574
      let mkUnion csetU accU =
575
        let cset = csetUnion csetO csetU in
576
        cssAdd cset accU
577
      in
578
      cssFold mkUnion accR accO
579
    in
580
    cssFold procOrset orset cssEmpty
581
  in
582
  let sort = stateGetSort state in
583
  let bs = stateGetBs state in
584
  let ats = extractAts sort bs in
585
  if stateGetStatus state = Expandable then csetAddDot ats else ();
586
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
587

    
588
let detConstraintsCore core =
589
  let sort = coreGetSort core in
590
  let bs = coreGetBs core in
591
  let ats = extractAts sort bs in
592
  let addCnstr acc state =
593
    if stateGetStatus state = Unsat then acc
594
    else
595
      let csets = stateGetConstraints state in
596
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
597
      cssUnion csets acc
598
  in
599
  let initInner =
600
    if coreGetStatus core = Expandable then
601
      (* let cset = csetCopy ats in *)
602
      let cset = ats in
603
      csetAddDot cset;
604
      cssSingleton cset
605
    else cssEmpty
606
  in
607
  List.fold_left addCnstr initInner (coreGetChildren core)
608

    
609
let rec propNom = function
610
  | [] -> ()
611
  | node::tl ->
612
      let tl1 =
613
        match node with
614
        | State state ->
615
            if stateGetStatus state = Unsat then tl
616
            else
617
              let csets = detConstraintsState state in
618
              let oldcsets = stateGetConstraints state in
619
              if cssEqual csets oldcsets then tl
620
              else begin
621
                stateSetConstraints state csets;
622
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
623
              end
624
        | Core core ->
625
            if coreGetStatus core = Unsat then tl
626
            else
627
              let csets = detConstraintsCore core in
628
              let oldcsets = coreGetConstraints core in
629
              if cssEqual csets oldcsets then tl
630
              else begin
631
                coreSetConstraints core csets;
632
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
633
              end
634
      in
635
      propNom tl1
636

    
637
let updateConstraints node elemU csets =
638
  let update cset acc =
639
    let cnstr =
640
      match graphFindCnstr cset with
641
      | Some cn -> cn
642
      | None ->
643
          let cn = UnexpandedC [] in
644
          graphInsertCnstr cset cn;
645
          queueInsertCnstr cset;
646
          cn
647
    in
648
    match cnstr with
649
    | UnsatC -> acc
650
    | UnexpandedC parents ->
651
        graphReplaceCnstr cset (UnexpandedC (node::parents));
652
        false
653
    | OpenC parents ->
654
        graphReplaceCnstr cset (OpenC (node::parents));
655
        false
656
    | SatC -> false
657
  in
658
  let isUnsat = cssFold update csets true in
659
  if isUnsat then propagateUnsat [elemU] else ()
660

    
661
let propagateNominals () =
662
  let init = cssSingleton (csetMake ()) in
663
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
664
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
665
  graphIterStates (fun s -> propNom [State s]);
666
  graphIterCores (fun c -> propNom [Core c]);
667
  graphClearCnstr ();
668
  let fktS state =
669
    if stateGetStatus state = Unsat then ()
670
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
671
  in
672
  graphIterStates fktS;
673
  let fktC core =
674
    if coreGetStatus core = Unsat then ()
675
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
676
  in
677
  graphIterCores fktC
678

    
679

    
680
(*****************************************************************************)
681
(*                           Node Expansions                                 *)
682
(*****************************************************************************)
683

    
684
let getLit sort fht solver f =
685
  match fhtFind fht f with
686
  | Some lit -> lit
687
  | None ->
688
      let var = M.new_variable solver in
689
      let lit = M.var_to_lit var true in
690
      fhtAdd fht f lit;
691
      let () =
692
        match lfGetNeg sort f with
693
        | None -> ()
694
        | Some nf ->
695
            let nlit = M.neg_lit lit in
696
            fhtAdd fht nf nlit;
697
      in
698
      lit
699

    
700
let newCore sort bs defer =
701
  (* when creating a now core from a set of formulas bs
702
        bs = { x_1, ...., x_n }
703
           = "x_1 /\ .... /\ x_n"
704
     Then we do this by:
705

    
706
        1. creating a new literal in the sat solver for each
707
           "boolean subformula" from the x_i. "boolean subformula" means that
708
           this subformula is not hidden under modalities but only under
709
           boolean connectives (/\, \/).
710
        2. encoding the relation between a formula and its intermediate boolean
711
           subformulas by a clause:
712
  *)
713
  let fht = fhtInit () in
714
  let solver = M.new_solver () in
715
  let rec addClauses f =
716
    (* step 1: create a literal in the satsolver representing the formula f *)
717
    let lf = getLit sort fht solver f in
718
    (* step 2: encode relation to possible subformulas *)
719
    match lfGetType sort f with
720
    | OrF ->
721
        (*
722
           case 2.(a)   f =  f1 \/ f2
723
                   fill fht such that it says:
724

    
725
                        f  |---> lf
726
                        f1 |---> lf1
727
                        f2 |---> lf2
728
        *)
729
        let f1 = lfGetDest1 sort f in
730
        let f2 = lfGetDest2 sort f in
731
        addClauses f1;
732
        addClauses f2;
733
        let lf1 = fhtMustFind fht f1 in
734
        let lf2 = fhtMustFind fht f2 in
735
        (*
736
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
737
        *)
738
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
739
        assert (okay)
740
    | AndF ->
741
        (*
742
           case 2.(b)   f =  f1 /\ f2
743
                   fill fht such that it says:
744

    
745
                        f  |---> lf
746
                        f1 |---> lf1
747
                        f2 |---> lf2
748
        *)
749
        let f1 = lfGetDest1 sort f in
750
        let f2 = lfGetDest2 sort f in
751
        addClauses f1;
752
        addClauses f2;
753
        let lf1 = fhtMustFind fht f1 in
754
        let lf2 = fhtMustFind fht f2 in
755
        (*
756
            encode the structure of f by adding the clauses
757
                    (lf -> lf1) /\ (lf -> lf2)
758
        *)
759
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
760
        assert (okay1);
761
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
762
        assert (okay2)
763
    | MuF
764
    | NuF ->
765
       (*
766
          Dest of a fixpoint is it's unfolded version. This adds just
767
          an simple forward implication that could be optimised out
768
          though not without nontrivial transformation of code
769

    
770
            f = μ X . φ   |---> lf
771
            φ[X |-> f]    |---> lf1
772

    
773
          Then adding lf -> lf1 to minisat
774
        *)
775
       let f1 = lfGetDest1 sort f in
776
       addClauses f1;
777
       let lf1 = fhtMustFind fht f1 in
778
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
779
       assert (okay1);
780
    | _ -> ()
781
        (* case 2.(c)
782
            We don't need to do anything except adding f to the fht
783
        *)
784
  in
785
  bsetIter addClauses bs;
786
  coreMake sort bs defer solver fht
787

    
788
let getNextState core =
789
  (* Create a new state, which is obtained by a satisfying assignment of the
790
     literals of the minisat solver.
791
     In addition to that, feed the negation of the satisfying assignment back
792
     to the minisat solver in order to obtain different solutions on successive
793
     minisat calls.
794
  *)
795
  let bs = coreGetBs core in
796
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
797
  let deferralS =
798
    if refocusing then
799
      bsetCopy bs
800
    else
801
      coreGetDeferral core
802
  in
803
  let fht = coreGetFht core in
804
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
805
  let solver = coreGetSolver core in
806
  let isSat = M.invoke_solver solver litset in
807
  (* Clearly, if the current core is unsatisfiable, no further child state can
808
     be created *)
809
  if not isSat then None
810
  else
811
    let sort = coreGetSort core in
812
    (* create a new set of formulas newbs with the property:
813
       if the conjunction of newbs is satisfiable, then the present core is
814
       satisfiable.
815
    *)
816
    let newbs = bsetMake () in
817
    let newdefer = bsetMakeRealEmpty () in
818
    (* if newbs = { l_1, .... l_n }, i.e.
819

    
820
            newbs = l_1 /\ ... /\ l_n
821

    
822
       then we can get essentially different satisfying assignments of bs by
823
       adding another clause
824

    
825
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
826

    
827
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
828
    *)
829
    let rec mkExclClause deferral f acc =
830
      (* f is a formula that is true in the current satisfying assignment *)
831
      match lfGetType sort f with
832
      | OrF ->
833
          (* if f is true and a disjunction, then one of its disjuncts is true *)
834
          let f1 = lfGetDest1 sort f in
835
          let lf1 = fhtMustFind fht f1 in
836
          (* if the first disjunct f1 is true, then we need to add subformulas
837
             of f1 to newbs&clause *)
838
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
839
          else
840
            (* otherwise f2 must be true *)
841
            let f2 = lfGetDest2 sort f in
842
            let lf2 = fhtMustFind fht f2 in
843
            assert (M.literal_status solver lf2 = M.LTRUE);
844
            mkExclClause deferral f2 acc
845
      | AndF ->
846
          (* if the true f is a conjuction, then both conjunctions must be true *)
847
          let f1 = lfGetDest1 sort f in
848
          let lf1 = fhtMustFind fht f1 in
849
          assert (M.literal_status solver lf1 = M.LTRUE);
850
          let acc1 = mkExclClause deferral f1 acc in
851
          let f2 = lfGetDest2 sort f in
852
          let lf2 = fhtMustFind fht f2 in
853
          assert (M.literal_status solver lf2 = M.LTRUE);
854
          mkExclClause deferral f2 acc1
855
      | MuF
856
      | NuF ->
857
         let f1 = lfGetDest1 sort f in
858
         mkExclClause deferral f1 acc
859
      | _ ->
860
         (* if f is a trivial formula or modality, then add it ... *)
861
         (* ... to newbs *)
862
         bsetAdd newbs f;
863
         let defercandidate = lfGetDeferral sort f in
864
         (if (defercandidate != (Hashtbl.hash "ε") &&
865
                (refocusing || deferral = defercandidate)) then
866
            bsetAdd newdefer f);
867
         (* ... and to the new clause *)
868
         (M.neg_lit (fhtMustFind fht f))::acc
869
    in
870
    let init_clause f acc =
871
      let deferral =
872
        if bsetMem deferralS f then (
873
          lfGetDeferral sort f)
874
        else
875
          (Hashtbl.hash "ε")
876
      in
877
      mkExclClause deferral f acc
878
    in
879
    let clause = bsetFold init_clause bs [] in
880
    let okay = M.add_clause solver clause in
881
    assert (okay);
882
    Some (sort, newbs, newdefer)
883

    
884
let newState sort bs defer =
885
  let (func, sl) = !sortTable.(sort) in
886
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
887
  let exp = producer sort bs defer sl in
888
  stateMake sort bs defer exp
889

    
890
let insertState parent sort bs defer =
891
  let child =
892
    match graphFindState sort (bs, defer) with
893
    | None ->
894
        let s = newState sort bs defer in
895
        graphInsertState sort (bs, defer) s;
896
        queueInsertState s;
897
        s
898
    | Some s -> s
899
  in
900
  coreAddChild parent child;
901
  stateAddParent child parent
902

    
903
let expandCore core =
904
  match getNextState core with
905
  | Some (sort, bs, defer) ->
906
      insertState core sort bs defer;
907
      queueInsertCore core
908
  | None ->
909
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
910
      if isUnsat then propagateUnsat [UCore (core, false)]
911
      else coreSetStatus core Open
912

    
913

    
914
let insertCore sort bs defer =
915
  match graphFindCore sort (bs, defer) with
916
  | None ->
917
     let c = newCore sort bs defer in
918
     graphInsertCore sort (bs, defer) c;
919
     queueInsertCore c;
920
     c
921
  | Some c -> c
922

    
923
let insertRule state dep chldrn =
924
  let chldrn = listFromLazylist chldrn in
925
  let insert (isUns, acc) (sort, bs, defer) =
926
    let bs1 = bsetAddTBox sort bs in
927
    let core = insertCore sort bs1 defer in
928
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
929
    (isUns1, core::acc)
930
  in
931
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
932
  let idx = stateAddRule state dep (List.rev children) in
933
  List.iter (fun c -> coreAddParent c state idx) children;
934
  if isUnsat then begin
935
    propagateUnsat [UState (state, Some idx)];
936
    false
937
  end else true
938

    
939
let rec insertAllRules state = function
940
  | [] -> true
941
  | (dep, chldrn)::tl ->
942
      let notUnsat = insertRule state dep chldrn in
943
      if notUnsat then insertAllRules state tl else false
944

    
945
let expandState state =
946
  match stateNextRule state with
947
  | MultipleElements rules ->
948
      let notUnsat = insertAllRules state rules in
949
      if notUnsat then stateSetStatus state Open
950
  | SingleElement (dep, chldrn) ->
951
      let notUnsat = insertRule state dep chldrn in
952
      if notUnsat then queueInsertState state else ()
953
  | NoMoreElements -> stateSetStatus state Open
954

    
955

    
956
let expandCnstr cset =
957
  let nht = nhtInit () in
958
  let mkCores f =
959
    let (sort, lf) as nom = atFormulaGetNominal f in
960
    let nomset =
961
      match nhtFind nht nom with
962
      | Some ns -> ns
963
      | None ->
964
          let cset1 = csetCopy cset in
965
          csetRemDot cset1;
966
          let bs = csetAddTBox sort cset1 in
967
          bsetAdd bs lf;
968
          nhtAdd nht nom bs;
969
          bs
970
    in
971
    bsetAdd nomset (atFormulaGetSubformula f)
972
  in
973
  csetIter cset mkCores;
974
  let inCores (sort, _) bs (isUns, acc) =
975
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
976
    coreAddConstraintParent core cset;
977
    (coreGetStatus core = Unsat || isUns, core::acc)
978
  in
979
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
980
  if isUnsat then propagateUnsat [UCnstr cset]
981
  else
982
    match graphFindCnstr cset with
983
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
984
    | _ -> assert false
985

    
986

    
987
(*****************************************************************************)
988
(*                           The Main Loop                                   *)
989
(*****************************************************************************)
990

    
991
let expandNodesLoop (recursiveAction: unit -> unit) =
992
  match queueGetElement () with
993
  | QState state ->
994
      if stateGetStatus state = Expandable then begin
995
        expandState state;
996
        if doNominalPropagation () then begin
997
          propagateNominals ();
998
          if doSatPropagation () then propagateUnsatMu ()
999
        end else ()
1000
      end else ();
1001
      recursiveAction ()
1002
  | QCore core ->
1003
      if coreGetStatus core = Expandable then begin
1004
        expandCore core;
1005
        if doNominalPropagation () then begin
1006
          propagateNominals ();
1007
          if doSatPropagation () then propagateUnsatMu ()
1008
        end else ()
1009
      end else ();
1010
      recursiveAction ()
1011
  | QCnstr cset ->
1012
      expandCnstr cset;
1013
      recursiveAction ()
1014
  | QEmpty -> ()
1015

    
1016
let runReasonerStep () =
1017
  let void () = () in
1018
  expandNodesLoop void; (* expand at most one node *)
1019
  (* if this emptied the queue *)
1020
  if queueIsEmpty () then begin
1021
    (* then check whether the nominals would add further queue elements *)
1022
    print_endline "Propagating nominals...";
1023
    propagateNominals ()
1024
  end else () (* else: the next step would be to expand another node *)
1025

    
1026
let rec buildGraphLoop () =
1027
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1028
  expandNodesFurther (); (* expand as many queue elements as possible *)
1029
  propagateNominals ();
1030
  (* if propagating nominals added some more queue members, do all again.. *)
1031
  if queueIsEmpty () then () else buildGraphLoop ()
1032

    
1033
let initReasoner sorts nomTable tbox sf =
1034
  sortTable := Array.copy sorts;
1035
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
1036
  let sort = fst sf in
1037
  let bs1 = bsetAddTBox sort bs in
1038
  let deferrals = bsetMakeRealEmpty() in
1039
  let markDeferral f =
1040
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1041
      bsetAdd deferrals f;)
1042
  in
1043
  bsetIter markDeferral bs;
1044
  graphInit ();
1045
  queueInit ();
1046
  let root = insertCore sort bs1 deferrals in
1047
  graphAddRoot root
1048

    
1049
let isRootSat () =
1050
  match coreGetStatus (graphGetRoot ()) with
1051
  | Expandable -> None
1052
  | Unsat -> Some false
1053
  | Sat -> Some true
1054
  | Open -> if (queueIsEmpty()) then Some true else None
1055

    
1056
let reasonerFinished () =
1057
  match coreGetStatus (graphGetRoot ()) with
1058
  | Expandable -> false
1059
  | Unsat
1060
  | Sat  -> true
1061
  | Open -> queueIsEmpty ()
1062

    
1063

    
1064
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1065
    @param verbose An optional switch which determines
1066
    whether the procedure shall print some information on the standard output.
1067
    The default is false.
1068
    @param sorts An array mapping each sort (represented as an integer)
1069
    to a functor and a list of sorts which are the arguments of the functor.
1070
    @param nomTable A partial function mapping nominals (represented as strings)
1071
    to their sorts.
1072
    @param tbox A list of sorted formulae.
1073
    @param sf A sorted formula.
1074
    @return True if sf is satisfiable wrt tbox, false otherwise.
1075
 *)
1076

    
1077
let isSat ?(verbose = false) sorts nomTable tbox sf =
1078
  let start = if verbose then Unix.gettimeofday () else 0. in
1079
  initReasoner sorts nomTable tbox sf;
1080
  let sat =
1081
    try
1082
      buildGraphLoop ();
1083
      (* get whether the root is satisfiable *)
1084
      (* we know that the reasoner finished, so the value is there, *)
1085
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1086
      CU.fromSome (isRootSat())
1087
    with CoAlg_finished res -> res
1088
  in
1089
  (* print some statistics *)
1090
  if verbose then
1091
    let stop = Unix.gettimeofday () in
1092
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1093
    print_newline ();
1094
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1095
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1096
    print_endline ("Added Size: " ^ (string_of_int size));
1097
    (*
1098
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1099
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1100
    print_endline ("Added Size: " ^ (string_of_int nsize));
1101
    *)
1102
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1103
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1104
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1105
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1106
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1107
    print_newline ()
1108
  else ();
1109
  sat