Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 5956a56d

History | View | Annotate | Download (38.7 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)) 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
      then begin
525
        visitParentStates core
526
      end
527
    in
528
    setIterState checkFinishingState setFinishingStates;
529
    setIterCore checkFinishingCore setFinishingCores;
530

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

    
541

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

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

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

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

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

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

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

    
678

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
912

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

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

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

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

    
954

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

    
985

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

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

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

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

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

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

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

    
1062

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

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